Abstract
The paper presents a method for the automatic verification of a certain class of parameterized systems. These are bounded-data systems consisting of N processes (N being the parameter), where each process is finite-state. First, we show that if we use the standard deductive INV rule for proving invariance properties, then all the generated verification conditions can be automatically resolved by finite-state (BDD-based) methods with no need for interactive theorem proving.
Next, we show how to use model-checking techniques over finite (and small) instances of the parameterized system in order to derive candidates for invariant assertions. Combining this automatic computation of invariants with the previously mentioned resolution of the VCs (verification conditions) yields a (necessarily) incomplete but fully automatic sound method for verifying bounded-data parameterized systems. The generated invariants can be transferred to the VC-validation phase without ever been examined by the user, which explains why we refer to them as “invisible”.
We illustrate the method on a non-trivial example of a cache protocol, provided by Steve German.
This research was supported in part by the Minerva Center for Verification of Reactive Systems, a gift from Intel, a grant from the German - Israel Foundation for Scientific Research and Development, and ONR grant N00014-99-1-0131.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. In CAV’99, LNCS 1633, pages 134–145, 1999.
K. R. Apt and D. Kozen. Limits for automatic program verification of finitestate concurrent systems. Information Processing Letters, 22(6), 1986.
M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In Proc. 5th ACM Symp. Princ. of Dist. Comp., pages 240–248, 1986.
E.M. Clarke, R. Enders, T. Filkron, and S. Jha. Exploiting symmetry in temporal logic model checking. Formal Methods in System Design, 9(1/2), 8 1996. Preliminary version appeared in 5th CAV, 1993.
E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In 6th International Conference on Concurrency Theory (CONCUR’95), pages 395–407, Philadelphia, PA, August 1995.
S.J. Creese and A.W. Roscoe. Formal verification of arbitrary network topologies. In Proc. of the Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA’99), Las Vegas, 1999. CSREA Press.
S.J. Creese and A.W. Roscoe. Verifying an infinite family of inductions simultaneously using data independence and fdr. In Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV’99), Beijing, 1999. Kluwer Academic Publishers.
S.J. Creese and A.W. Roscoe. Data independent induction over structured networks. In Proc. of the Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA’00), Las Vegas, June 2000. CSREA Press.
E.A. Emerson and V. Kahlon. Reducing model checking of the many to the few. In 17th International Conference on Automated Deduction (CADE-17), pages 236–255, 2000.
E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL’95, 1995.
E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In CAV’96, LNCS 1102, 1996.
E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9(1/2), 8 1996. Preliminary version appeared in 5th CAV, 1993.
E. A. Emerson and A. P. Sistla. Utilizing symmetry when model checking under fairness assumptions. ACM Trans. Prog. Lang. Sys., 19(4), 1997. Preliminary version appeared in 7th CAV, 1995.
Ger00. S. German. Personal Communication, 2000.
V. Gyuris and A. P. Sistla. On-the-y model checking under fairness that exploits symmetry. In CAV’97, LNCS 1254, 1997.
E.P. Gribomont and G. Zenner. Automated verification of szymanski’s algorithm. In TACAS’98, LNCS 1384, pages 424–438, 1998.
N. Halbwachs, F. Lagnier, and C. Ratel. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6/7):523–543, 1992.
C.N. Ip and D. Dill. Verifying systems with replicated components in Murϕ In CAV’96, LNCS 1102, 1996.
E. Jensen and N.A. Lynch. A proof of burn’s n-process mutual exclusion algorithm using abstraction. In TACAS’98, LNCS 1384, pages 409–423, 1998.
B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS’00, LNCS 1785, 2000.
R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1–11, 1995.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In CAV’97, LNCS 1254, pages 424–435, 1997.
Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of practical formal verification. Software Tools for Technology Transfer, 4(2):328–342, 2000.
D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL’97, 1997.
D. Lesens and H. Saidi. Automatic verification of parameterized networks of processes by abstraction. In 2nd International Workshop on the Verification of Infinite State Systems (INFINITY’97), 1997.
Z. Manna, A. Anuchitanukul, N. Bjårner, A. Browne, E. Chang, M. Colón, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994.
K.L. McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In CAV’98, LNCS 1427, pages 110–121, 1998.
Z. Manna and A. Pnueli. An exercise in the verification of multiprocess programs. In W.H.J. Feijen, A.J.M van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business, pages 289–301. Springer-Verlag, 1990.
A. Pnueli and E. Shahar. Livenss and acceleraiton in parameterized verification. In CAV’00, LNCS 1855, 2000.
A. Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I.V. Ramakrishnan, and S.A. Smolka. Verification of parameterized systems using logic program transformations. In TACAS’00, LNCS 1785, 2000.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In CAV’89, LNCS 407, pages 151–165, 1989.
A.P. Sistla and S.M. German. Reasoning about systems with many processes. J. ACM, 39:675–735, 1992.
N. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (draft). Technical report, Comp. Sci.,Laboratory, SRI International, Menlo Park, CA, 1993.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In CAV’89, LNCS 407, pages 68–80, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pnueli, A., Ruah, S., Zuck, L. (2001). Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_7
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive