Abstract
We present a method for verifying universal properties of fair parameterized networks of finite processes, that is, properties of the form ∀p 1...p n :ψ, where ψ is a quantifier-free LTL formula. The starting point of our verification method is an encoding of the infinite family of networks by a single fair transition system whose variables are set (2nd- order) variables and transitions are described in WS1S, such a system is called a WS1S transition system. We abstract the WS1S system into a finite state system that can be model-checked. We present a generic abstraction relation for verifying universal properties as well as an algorithm for computing an abstract system. Since, the abstract system may contain infinite computations that have no corresponding fair computations at the concrete level, the verification of progress property often fails. Therefore, we present methods that allow to synthesize fairness conditions from the parameterized network and discuss under which conditions and how to lift fairness conditions of this network to fairness conditions on the abstract system. We implemented our methods in a tool, called pax, and applied it to several examples.
This work has been partially supported by the Esprit-LTR project Vires.
Verimag is a joint research laboratory of the University Joseph Fourier (Grenoble I), National Polytechnical Institute of Grenoble (INPG) and the National Center of Scientic Research (CNRS).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling Global Conditions in Parameterized System Verification. In N. Halbwachs and D. Peled, editors, CAV’ 99, volume 1633 of LNCS, pages 134–145. Springer, 1999.
K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S Systems to Verify Parameterized Networks. In S. Graf and M. Schwartzbach, editors, TACAS’00, volume 1785. Springer, 2000.
M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many identical finite state processes. Information and Computation, 1989.
K. Baukus, Y. Lakhnech, and K. Stahl. Verifying Universal Properties of Parameterized Networks. Technical Report TR-ST-00-4, CAU Kiel, 2000.
J.R. Büchi. Weak Second-Order Arithmetic and Finite Automata. Z. Math. Logik Grundl. Math., 6:66–92, 1960.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM symp. of Prog. Lang., pages 238–252. ACM Press, 1977.
E. Clarke, O. Grumberg, and S. Jha. Verifying Parameterized Networks using Abstraction and Regular Languages. In I. Lee and S. Smolka, editors, CONCUR’ 95: Concurrency Theory, LNCS. Springer, 1995.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1994.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In E.-R. Olderog, editor, Proceedings of PROCOMET’ 94. North-Holland, 1994.
C.C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21–52, 1961.
E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In 8th Conference on Computer Aided Verification, LNCS 1102, pages 87–98, 1996.
S.M. German and A.P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675–735, 1992.
J.G. Henriksen, J. Jensen, M. JØrgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic Second-Order Logic in Practice. In TACAS’ 95, volume 1019 of LNCS. Springer, 1996.
B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In S. Graf and M. Schwartzbach, editors, TACAS’00, volume 1785. Lecture Notes in Computer Science, 2000.
R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In ACM Symp. on Principles of Distributed Computing, Canada, pages 239–247, Edmonton, Alberta, 1989.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In O. Grumberg, editor, Proceedings of CAV’ 97, volume 1256 of LNCS, pages 424–435. Springer, 1997.
W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics, pages 134–191. Elsevier Science Publishers B. V., 1990.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants (extended abstract). In Sifakis, editor, Workshop on Computer Aided Verification, LNCS 407, pages 68–80, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baukus, K., Lakhnech, Y., Stahl, K. (2000). Verifying Universal Properties of Parameterized Networks. In: Joseph, M. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2000. Lecture Notes in Computer Science, vol 1926. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45352-0_24
Download citation
DOI: https://doi.org/10.1007/3-540-45352-0_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41055-3
Online ISBN: 978-3-540-45352-9
eBook Packages: Springer Book Archive