Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Robots at the Edge of the Cloud Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Parameterized Compositional Model Checking

Authors : Kedar S. Namjoshi, Richard J. Trefler

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The Parameterized Compositional Model Checking Problem (PCMCP) is to decide, using compositional proofs, whether a property holds for every instance of a parameterized family of process networks. Compositional analysis focuses attention on the neighborhood structure of processes in the network family. For the verification of safety properties, the PCMCP is shown to be much more tractable than the more general Parameterized Model Checking Problem (PMCP). For example, the PMCP is undecidable for ring networks while the PCMCP is decidable in polynomial time. This result generalizes to toroidal mesh networks and related networks for describing parallel architectures. Decidable models of the PCMCP are also shown for networks of control and user processes. The results are based on the demonstration of compositional cutoffs; that is, small instances whose compositional proofs generalize to the entire parametric family. There are, however, control-user models where the PCMCP and the PMCP are both undecidable.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter v2c – A Verilog to C Translator
next chapter An Algorithm for Stuttering Equivalence and Branching Bisimulation
Footnotes
1
The notation is from Dijkstra-Scholten [8]: \([\varphi ]\) means that \(\varphi \) is valid.
 
2
A groupoid is roughly a group with a partial composition operation. The network symmetry groupoid meets the conditions required of a groupoid: (1) \((m, \iota , m)\) is a symmetry for each node m, where \(\iota \) is the identity map; (2) if \((m,\beta ,n)\) is a symmetry so is the inverse \((n,\beta ^{-1},m)\); and (3) the composition of symmetries \((m,\beta ,n)\) and \((n',\gamma ,o)\), given by \((m,\gamma \beta ,o)\) if \(n = n'\), is also a symmetry.
 
3
The algorithm in [13] considers checking Linear Temporal Logic formulae on networks of processes, in contrast we restrict attention to checking safety properties.
 
4
Unlike the other cases, the local state space of the control process is unbounded as it has the form (c, x) where c is its internal state (which is bounded), and x is the vector of neighboring edge-values, which can have arbitrary length.
 
5
We do not know the status of the PMCP. The powerful WQO theory of [1] appears not to apply due to the presence of universal guards. A more general assignment action, https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49674-9_39/419290_1_En_39_IEq231_HTML.gif , also preserves the decidability of PCMCP. Allowing the dual action of assigning a value to some edge makes the PMCP undecidable (a reduction from 2CM). We do not know whether it also makes the PCMCP undecidable.
 
Literature
1.
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321. IEEE Computer Society (1996)
2.
Abdulla, P.A., Haziza, F., Holík, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476–495. Springer, Heidelberg (2013)CrossRef
3.
Akers, S.B., Krishnamurthy, B.: A group-theoretic model for symmetric interconnection networks. IEEE Trans. Comput. 38(4), 555–566 (1989)MathSciNetCrossRefMATH
4.
Alur, R., Henzinger, T.: Reactive modules. In: IEEE LICS (1996)
5.
Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)MathSciNetCrossRef
6.
Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1/2), 77–104 (1996)CrossRef
7.
Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2006)CrossRef
8.
Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer, New York (1990)CrossRefMATH
9.
Emerson, E., Namjoshi, K.: Reasoning about rings. In: ACM Symposium on Principles of Programming Languages (1995)
10.
Emerson, E., Sistla, A.: Symmetry and model checking. Formal Methods in System Design 9(1/2), 105–131 (1996)CrossRef
11.
Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124–140. Springer, Heidelberg (2013)CrossRef
12.
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with Invisible Ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 223–238. Springer, Heidelberg (2004)CrossRef
13.
14.
15.
Gopalakrishnan, G., Kriby, R.M., Siegel, S.F., Thakur, R., Gropp, W., Lusk, E., De Supinski, B.R., Schulz, M., Bronevetsky, G.: Formal analysis of MPI-based parallel programs. Commun. of the ACM 54, 82–91 (2011)CrossRef
16.
Hayes, J.P., Mudge, T.N., Stout, Q.F., Colley, S., Palmer, J.: Architecture of a hypercube supercomputer. In: Conference on Parallel Processing, pp. 653–660 (1986)
17.
18.
Kurshan, R.: Computer-Aided Verification of Coordinating Processes: TheAutomata-Theoretic Approach. Princeton University Press, Princeton (1994)
19.
20.
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)CrossRefMATH
21.
Minsky, M.: Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs (1967)MATH
22.
Namjoshi, K.S., Trefler, R.J.: Local symmetry and compositional verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 348–362. Springer, Heidelberg (2012)CrossRef
23.
Namjoshi, K.S., Trefler, R.J.: Uncovering symmetries in irregular process networks. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 496–514. Springer, Heidelberg (2013)CrossRef
24.
Namjoshi, K.S., Trefler, R.J.: Analysis of dynamic process networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 164–178. Springer, Heidelberg (2015)
25.
Namjoshi, K.S., Trefler, R.J.: Loop freedom in AODVv2. In: Graf, S., Viswanathan, M. (eds.) Formal Techniques for Distributed Objects, Components, and Systems. LNCS, vol. 9039, pp. 98–112. Springer, Heidelberg (2015)CrossRef
26.
27.
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)CrossRef
28.
Preparata, F.P., Vuillemin, J.: The cube-connected cycles: a versatile network for parallel computation. CACM 24(5), 300–309 (1981)MathSciNetCrossRef
29.
Sánchez, A., Sánchez, C.: LEAP: a tool for the parametrized verification of concurrent datatypes. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 620–627. Springer, Heidelberg (2014)
30.
31.
32.
Siegel, S.F., Avrunin, G.S.: Verification of MPI-based software for scientific computation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 286–303. Springer, Heidelberg (2004)CrossRef
33.
Siegel, S.F., Gopalakrishnan, G.: Formal analysis of message passing. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 2–18. Springer, Heidelberg (2011)CrossRef
Metadata
Title
Parameterized Compositional Model Checking
Authors
Kedar S. Namjoshi
Richard J. Trefler
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49674-9_39

Premium Partner

    Image Credits