Correct System Design pp 180-197 | Cite as

# On the Existence of Network Invariants for Verifying Parameterized Systems

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- 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 - 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 - 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 - 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 - AČJYK96.Parosh Aziz Abdulla, Karlis Čerāns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinitestate systems. In
*Proc. 11*^{th}*IEEE Int. Symp. on Logic in Computer Science*, pages 313–321, 1996.Google Scholar - 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 - 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 - AK86.K. Apt and D.C. Kozen. Limits for automatic verification of finitestate concurrent systems.
*Information Processing Letters*, 22:307–309, 1986.CrossRefMathSciNetGoogle Scholar - AL92.M. Abadi and L. Lamport. An oldfashioned recipe for real time. In de Bakker, Huizing, de Roever, and Rozenberg, editors,
*RealTime: Theory in Practice*, volume 600 of Lecture Notes in Computer Science, 1992.CrossRefGoogle Scholar - 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 - 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 - 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 - 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 - 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 - 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 - EN95.E.A. Emerson and K.S. Namjoshi. Reasoning about rings. In
*Proc. 22th ACM Symp. on Principles of Programming Languages*, 1995.Google Scholar - Fin94.A. Finkel. Decidability of the termination problem for completely specified protocols.
*Distributed Computing*, 7(3), 1994.Google Scholar - 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 - Hen95.T.A. Henzinger. Hybrid automata with finite bisimulations. In
*Proc. ICALP ‘95*, 1995.Google Scholar - 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 - JK95.Bengt Jonsson and Lars Kempe. Verifying safety properties of a class of infinitestate 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 - 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 - 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 - KLL+97.K.J. Kristoffersen, F. Larroussinie, K. G. Larsen, P. Pettersson, and W. Yi. A compositional proof of a realtime 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 - 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 - 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 - Lam89.L. Lamport. A simple approach to specifying concurrent systems,.
*Communications of the ACM*, 32(1):32–45, Jan. 1989.CrossRefMathSciNetGoogle Scholar - 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 - LS97.D. Lesens and H. Saidi. Abstraction of parameterized networks.
*Electronic Notes in Theoretical Computer Science*, 9, 1997.Google Scholar - MP95.Z. Manna and A. Pnueli.
*Temporal Verification of Reactive Systems*:*Safety*. Springer Verlag, 1995.Google Scholar - Sha93.N. Shankar. Verification of realtime 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 - 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 - 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 - 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 - 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