Advertisement

On the Existence of Network Invariants for Verifying Parameterized Systems

  • Parosh Aziz Abdulla
  • Bengt Jonsson
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)

Abstract

Over the last decade, finite-state verification methods have been developed to an impressive tool for analysis of complex programs, such as protocols and hardware circuits. Partial-order reduction and BDD-based symbolic model checking have been instrumental in this development. Currently, much effort is devoted to advancing further the power of automated verification to cover also infinite-state systems. In this paper, we consider the class of so-called parameterized systems, i.e., systems with many similar processes, in which the number of processes is unbounded and their interconnection pattern may vary within the range of some constraints. We partially review the use of induction over the system structure for the verification of parameterized systems. Wolper and Lovinfosse have introduced the term network invariant for the induction hypothesis in such a proof by induction. They also observe that well-behaved (e.g., finite-state) network invariants do not always exist, even if the system itself satisfies the property to be veri fied. The main contribution of the paper is to present some suficient conditions, under which the existence of a finite-state network invariant is guaranteed. We also relate the construction of network invariants to the search for standard inductive invariants. Two small examples of network invariants and standard invariants for parameterized systems are included.

Keywords

Shared Variable Critical Section Mutual Exclusion Label Transition System Network Invariant 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ABJ98.
    Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. 10 th Int. Conf. on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 305–318, 1998.CrossRefGoogle Scholar
  2. ABJN99.
    Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, and Marcus Nilsson. Handling global conditions in parameterized system verification. In Proc. 11 th Int. Conf. on Computer Aided Verification, 1999.Google Scholar
  3. ACD90.
    R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 414–425, Philadelphia, 1990.Google Scholar
  4. ACHH92.
    R. Alur, C. Courcoubetis, T. Henzinger, and P.­H. Ho. Hybrid automata: An algorithmic approach to the specification and verificationof hybrid systems. In Grossman, Nerode, Ravn, and Rischel, editors, Hybrid Systems, number 736 in Lecture Notes in Computer Science, pages 209–229, 1992.Google Scholar
  5. AČJYK96.
    Parosh Aziz Abdulla, Karlis Čerāns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite­state systems. In Proc. 11 th IEEE Int. Symp. on Logic in Computer Science, pages 313–321, 1996.Google Scholar
  6. AJ93.
    Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8 th IEEE Int. Symp. on Logic in Computer Science, pages 160–170, 1993.Google Scholar
  7. AJ98.
    Parosh Aziz Abdulla and Bengt Jonsson. Verifying networks of timed processes. In Bernhard Steffen, editor, Proc. TACAS ‘98, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 298–312, 1998.CrossRefGoogle Scholar
  8. AK86.
    K. Apt and D.C. Kozen. Limits for automatic verification of finite­state concurrent systems. Information Processing Letters, 22:307–309, 1986.CrossRefMathSciNetGoogle Scholar
  9. AL92.
    M. Abadi and L. Lamport. An old­fashioned recipe for real time. In de Bakker, Huizing, de Roever, and Rozenberg, editors, Real­Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, 1992.CrossRefGoogle Scholar
  10. And95.
    H.R. Andersen. Partial model checking (extended abstract). In Proc. 10 th IEEE Int. Symp. on Logic in Computer Science, pages 398–407. IEEE Computer Society Press, 1995.Google Scholar
  11. BGK+96.
    J. Bengtsson, W. O. D. Grioen, K.J. Kristoffersen, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an audio protocol with bus collision using UPPAAL. In R. Alur and T. Henzinger, editors, Proc. 8 th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 244–256, New Brunswick, USA, 1996. Springer Verlag.Google Scholar
  12. BS95.
    O. Burkart and B. Steffen. Composition, decomposition, and model checking of pushdown processes. Nordic Journal of Computing, 2(2):89–125, 1995.zbMATHMathSciNetGoogle Scholar
  13. CGJ95.
    E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In Lee and Smolka, editors, Proc. CONCUR ‘95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 395–407. Springer Verlag, 1995.Google Scholar
  14. Dic13.
    L. E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors.Amer. J. Math., 35:413–422, 1913.CrossRefMathSciNetGoogle Scholar
  15. EFM99.
    J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proc. 14 th IEEE Int. Symp. on Logic in Computer Science, 1999.Google Scholar
  16. EN95.
    E.A. Emerson and K.S. Namjoshi. Reasoning about rings. In Proc. 22th ACM Symp. on Principles of Programming Languages, 1995.Google Scholar
  17. Fin94.
    A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3), 1994.Google Scholar
  18. GS92.
    S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675–735, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  19. Hen95.
    T.A. Henzinger. Hybrid automata with finite bisimulations. In Proc. ICALP ‘95, 1995.Google Scholar
  20. ID99.
    C. Norris Ip and David L. Dill. Verifying systems with replicated components in Mur‘. Formal Methods in System Design, 14(3), May 1999.Google Scholar
  21. JK95.
    Bengt Jonsson and Lars Kempe. Verifying safety properties of a class of infinite­state distributed algorithms. In Proc. 7 th Int. Conf. on Computer Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 42–53. Springer Verlag, 1995.Google Scholar
  22. JM95.
    P. Jančcar and F. Moller. Checking regular properties of Petri nets. In Proc. CONCUR ‘95, 6 th Int. Conf. on Concurrency Theory, pages 348–362, 1995.Google Scholar
  23. JP93.
    B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of non-finite-state programs. Information and Computation, 107(2):272–302, Dec. 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  24. KLL+97.
    K.J. Kristoffersen, F. Larroussinie, K. G. Larsen, P. Pettersson, and W. Yi. A compositional proof of a real­time mutual exclusion protocol. In TAPSOFT ‘97 7 th International Joint Conference on the Theory and Practice of Software Development, Lecture Notes in Computer Science, Lille, France, April 1997. Springer Verlag.Google Scholar
  25. KM89.
    R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In Proc. 8 th ACM Symp. on Principles of Distributed Computing, Canada, pages 239–247, Edmonton, Alberta, 1989.Google Scholar
  26. KMM+97.
    Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. 9 th Int. Conf. on Computer Aided Verification, volume 1254, pages 424–435, Haifa, Israel, 1997. Springer Verlag.Google Scholar
  27. Lam89.
    L. Lamport. A simple approach to specifying concurrent systems,. Communications of the ACM, 32(1):32–45, Jan. 1989.CrossRefMathSciNetGoogle Scholar
  28. LHR97.
    D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In Proc. 24 th ACM Symp. on Principles of Programming Languages, 1997.Google Scholar
  29. LS97.
    D. Lesens and H. Saidi. Abstraction of parameterized networks. Electronic Notes in Theoretical Computer Science, 9, 1997.Google Scholar
  30. MP95.
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer Verlag, 1995.Google Scholar
  31. Sha93.
    N. Shankar. Verification of real­time systems using PVS. In Courcoubetis, editor, Proc. 5 th Int. Conf. on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 280–291, 1993.Google Scholar
  32. Sti96.
    C. Stirling. Decidability of bisimulation equivalence for normed pushdown processes. In Proc. CONCUR ‘96, 7 th Int. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 217–232. Springer Verlag, 1996.Google Scholar
  33. WB98.
    Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In Proc. 10 th Int. Conf. on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 88–97, Vancouver, July 1998. Springer Verlag.CrossRefGoogle Scholar
  34. WL89.
    P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants (extended abstract). In Sifakis, editor, Proc. Workshop on Computer Aided Verification, number 407 in Lecture Notes in Computer Science, pages 68–80, 1989.Google Scholar
  35. Wol86.
    Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13 th ACM Symp. on Principles of Programming Languages, pages 184–193, Jan. 1986Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Parosh Aziz Abdulla
    • 1
  • Bengt Jonsson
    • 1
  1. 1.Dept. Computer Systems Uppsala UniversitySweden

Personalised recommendations