Constraint-Based Model Checking for Parameterized Synchronous Systems

  • Giorgio Delzanno
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2309)


We present a fully-automatic method for checking safety properties of parameterized synchronous systems based on a backward reachability procedure working over real arithmetics. We consider here concurrent systems consisting of many identical (finite-state) processes and one monitor where processes may react non-deterministically to the messages sent by the monitor. This type of non-determinism allows us to model abstractions of situations in which processes are re-allocated according to individual properties. We represent concisely collections of global states counting the number of processes in a given state during a run of the global system, i.e., we reason modulo symmetries. We u se a special class of linear arithmetic constraints to represent collections of global system states. We define a decision procedure for checking safety properties for parameterized systems using efficient constraints operations defined over real arithmetics. The procedure can be implemented using existing constraint-based symbolic model checkers or tools for program analysis defined over real-arithmetics.


Model Check Global State Concurrent System Symbolic Model Check Reachability Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. A. Abdulla, K. Cerāns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. of LICS 96, pp. 313–321, 1996.Google Scholar
  2. 2.
    M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. Series in Parallel Computing. John Wiley & Sons, 1995.Google Scholar
  3. 3.
    K. Apt and D. Kozen. Limits for Automatic Verification of Finite-state Concurrent Systems. Information Processing Letters 15, pp. 307–309, 1986.CrossRefMathSciNetGoogle Scholar
  4. 4.
    T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. In Proc. TACAS’ 01, LNAI 2031, pages 158–173, 2001.Google Scholar
  5. 5.
    M. C. Browne, E. M. Clarke, O. Grumberg. Reasoning about Networks with Many Identical Finite State Processes. Information and Computation 81(1): 13–31, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    B. Bérard, and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In Proc. of CONCUR 99, LNAI 1664, pp. 178–193.Google Scholar
  7. 7.
    B. Boigelot and P. Wolper. Verifying Systems with Infinite but Regular State Space. In Proc. of CAV 98, LNAI 1427, pp. 88–97. Springer, 1998.Google Scholar
  8. 8.
    A. Bouajjani and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proc. of STACS 99, LNAI 1563, pp. 323–333. 1999.Google Scholar
  9. 9.
    T. Bultan. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. Proc. of TACAS 2000, LNAI 1785, pp. 441–455, 2000.Google Scholar
  10. 10.
    T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite-state Systems using Presburger Arithmetics. In Proc. of CAV 97, LNAI 1254, pp. 400–411, 1997.Google Scholar
  11. 11.
    G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In Proc. of ICATPN, LNAI 815, pp. 179–198, 1994.Google Scholar
  12. 12.
    E. Clarke, O. Grumberg, S. Jha. Verifying Parameterized Networks. TOPLAS 19(5): 726–750 (1997).CrossRefGoogle Scholar
  13. 13.
    P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In Proc. of POPL 78, pp. 84–96, 1978.Google Scholar
  14. 14.
    G. Delzanno. Automated Verification of Parameterized Cache Coherence Protocols. In Proc. CAV’00, LNAI 1855, pp. 53–68, 2000.Google Scholar
  15. 15.
    G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proc. of CSL 99, LNAI 1683, pp. 50–66, 1999.Google Scholar
  16. 16.
    G. Delzanno and A. Podelski, Model Checking in CLP. In Proc. of TACAS 99, LNAI 1579, pp. 223–239, 1999.Google Scholar
  17. 17.
    G. Delzanno, J.-F. Raskin, and L. Van Begin. Attacking Symbolic State Explosion. In Proc. CAV 2001, LNAI 2102, pages 298–310, Springer, 2001.Google Scholar
  18. 18.
    G. Delzanno, J.-F. Raskin, and L. Van Begin. Towards the Automated Verification of Multithreaded Java Programs. To appear in TACAS 2002, April 2001.Google Scholar
  19. 19.
    E. A. Emerson and K. S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. In Proc. CAV 96, LNAI 1102, pp. 87–98, 1996.Google Scholar
  20. 20.
    E. A. Emerson and K. S. Namjoshi. On Model Checking for Non-deterministic Infinite-state Systems. In Proc. LICS 98, pp. 70–80, 1998.Google Scholar
  21. 21.
    J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS 99, pp. 352–359, 1999.Google Scholar
  22. 22.
    A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1–2):63–92, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    S. M. German, A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39(3): 675–735 (1992).zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    S. Graf and H. Saïdi. Construction of Abstract State Graphs with PVS. In Proc. of CAV 97, LNAI 1254, pp. 72–83, 1997.Google Scholar
  25. 25.
    N. Halbwachs. Delay analysis in synchronous programs. In Proc. CAV 93, LNAI 697, pp. 333–346, 1993.Google Scholar
  26. 26.
    N. Halbwachs and Y.-E. Proy and P. Raymond. Verification of Linear Hybrid Systems by Means of Convex Approximations. In Proc. SAS 94, LNAI 864, pp. 223–237, 1994Google Scholar
  27. 27.
    J. Handy. The Cache Memory Book. Academic Press, 1993.Google Scholar
  28. 28.
    T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: a Model Checker for Hybrid Systems. In Proc. CAV 97, LNAI 1254, pp. 460–463, 1997.Google Scholar
  29. 29.
    R. M. Karp and R. E. Miller. Parallel Program Schemata. Journal of Computer and System Sciences, 3, pp. 147–195, 1969.zbMATHMathSciNetGoogle Scholar
  30. 30.
    R. P. Kurshan and K. McMillan. A Structural Induction Theorem for Processes. In Proc. 8th ACM Symp. on Principles of Distributed Computing, pp. 239–247, 1989.Google Scholar
  31. 31.
    D. Lesens and N. Halbwachs and P. Raymond. Automatic Verification of Parameterized Linear Networks of Processes. In Proc. of POPL 97, pp. 346–357, 1997.Google Scholar
  32. 32.
    D. Lesens and H. Saidi. Automatic Verification of Parameterized Networks of Processes by Abstraction. In Proc. INFINITY 97, 1997.Google Scholar
  33. 33.
    K. L. McMillan. Verification of Infinite State Systems by Compositional Model Checking. In Proc. CHARME 99, LNAI 1703, pp. 219–234, 1999.Google Scholar
  34. 34.
    A. Schrijver. Theory of Linear and Integer Programming. Wiley and Sons, 1998.Google Scholar
  35. 35.
    D. Srivistava. Subsumption and Indexing in Constraint Query Languages with Linear Arithmetic Constraints. Annals of Mathematics and Artificial Intelligence, 8(3–4): 315–343, 1993.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Giorgio Delzanno
    • 1
  1. 1.Dipartimento di Informatica e Scienze dell’InformazioneUniversità di GenovaItaly

Personalised recommendations