Abstract
The paper considers the problem of uniform verification of parameterizedsystems by symbolic model checking, using formulas in fs1s (a syntactic variant of the 2nd order logic ws1s) for the symbolic representation of sets of states. The technical difficulty addressed in this work is that, in many cases, standard model-checking computations fail to converge.
Using the tool tlvĀ [P], we formulated a general approach to the acceleration of the transition relations, allowing an unbounded number of different processes to change their local state (or interact with their neighbor) in a single step. We demonstrate that this acceleration process solves the difficulty and enables an efficient symbolic model-checking of many parameterized systems such as mutual-exclusion and token-passing protocols for any value of N, the parameter specifying the size of the system.
Most previous approaches to the uniform verification of parameterized systems, only considered safety properties of such systems. In this paper, we present an approach to the verification of iveness properties and demonstrate its application to prove accessibility properties of the considered protocols.
This research was supported in part by the Minerva Center for Verification of Reactive Systems, a gift from Intel, and a grant from the U.S.-Israel bi-national science foundation.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.Ā 1427, pp. 305ā318. Springer, Heidelberg (1998)
Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parameterized system verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.Ā 1633, pp. 134ā145. Springer, Heidelberg (1999)
Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.Ā 1384, pp. 298ā312. Springer, Heidelberg (1998)
Apt, K.R., Kozen, D.: Limits for automatic program verification of finite-state concurrent systems. Information Processing LettersĀ 22(6) (1986)
Bodeveix, J.-P., Filali, M.: Experimenting acceleration methods for the validation of infinite state systems. In: International Workshop on Distributed System Validation and Verification (DSVV 2000), Taipei, Taiwan (April 2000)
Boigelot, B., Godefroid, P.: Symbolic verification of coomunication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.Ā 1102, pp. 1ā12. Springer, Heidelberg (1996)
Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.Ā 1302. Springer, Heidelberg (1997)
Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO- channel systems with non-regular sets of configurations. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.Ā 1256. Springer, Heidelberg (1997)
Clarke, E.M., Grumberg, O., Jha, S.: Verifying parametrized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.Ā 962, pp. 395ā407. Springer, Heidelberg (1995)
Dijkstra, E.W., Feijen, W.H.J., van Gasteren, A.J.M.: Derivation of a termination detection algorithm for distributed computations. Info. Proc. Lett.Ā 16(5), 217ā219 (1983)
Gribomont, E.P., Zenner, G.: Automated verification of szymanskiās algorithm. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.Ā 1384, pp. 424ā438. Springer, Heidelberg (1998)
Henriksen, J.G., Jensen, J., JĆørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.Ā 1019. Springer, Heidelberg (1995)
Jensen, E., Lynch, N.A.: A proof of burnās n-process mutual exclusion algorithm using abstraction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.Ā 1384, pp. 409ā423. Springer, Heidelberg (1998)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.Ā 1785, p. 220. Springer, Heidelberg (2000) (to appear)
Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Rudnicki, P. (ed.) Proceedings of the 8th Annual Symposium on Principles of Distributed Computing, Edmonton, AB, Canada, August 1989, pp. 239ā248. ACM Press, New York (1989)
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.Ā 1254, pp. 424ā435. Springer, Heidelberg (1997)
Manna, Z., Anuchitanukul, A., BjĆørner, N., Browne, A., Chang, E., ColĆ³n, M., De Alfaro, L., Devarajan, H., Sipma, H., Uribe, T.E.: STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California (1994)
Manna, Z., Pnueli, A.: An exercise in the verification of multi ā process programs. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty is Our Business, pp. 289ā301. Springer, Heidelberg (1990)
Sistla, A.P., German, S.M.: Reasoning about systems with many processes. J. ACMĀ 39, 675ā735 (1992)
Thomas, W.: Automata on infinite objects. Handbook of theoretical computer science, 165ā191 (1990)
Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.Ā 407, pp. 68ā80. Springer, Heidelberg (1990)
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
Pnueli, A., Shahar, E. (2000). Liveness and Acceleration in Parameterized Verification. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_26
Download citation
DOI: https://doi.org/10.1007/10722167_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive