Abstract
In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems — Model Checking (in particular symbolic) and Deductive Verification, they are still limited in their ability to handle large systems. It is generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization, which breaks the task of verifying a large system into several smaller tasks of verifying simpler systems.
In this methodological paper, we review the two main tools of compositionality and abstraction in the framework of linear temporal logic. We illustrate the application of these two methods for the reduction of an infinite-state system into a finite-state system that can then be verified using model checking.
The modest technical contributions contained in this paper are a full formulation of abstraction when applied to a system with both weak and strong fairness requirements and to a general temporal formula, and a presentation of a compositional framework for shared variables and its application for forming network invariants.
This research was supported in part by a gift from Intel, a grant from the U.S.-Israel bi-national science foundation, and an Infrastructure grant from the Israeli Ministry of Science and the Arts.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Properties preserving simulations. CAV'92, vol. 663 of LNCS, pp 251–263, 1992.
N. BjØrner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. 1st Intl. Conf. on Principles and Practice of Constraint Programming, vol. 976 of LNCS, pp 589–623, 1995.
M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. PODC'86, pp 240–248, 1986.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL'77, 1977.
E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at Ltl model checking. CAV'94, vol. 818 of LNCS, pp 415–427, 1994.
E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. CONCUR'95, pp 395–407, 1995.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Trans. Prog. Lang. Sys., 16(5):1512–1542, 1994.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. Model Checking, Abstraction and Composition, vol. 152 of Nato ASI Series F, pages 477–498. Springer-Verlag, 1996.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. POPL'78, pp 84–96, 1978.
D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Sys., 19(2), 1997.
E. A. Emerson and K. S. Namjoshi. Reasoning about rings. POPL'95, 1995.
E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. CAV'96, LNCS, 1996.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. CAV'93, vol. 697 of LNCS, pp 71–84, 1993.
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ϕ. CAV'96, LNCS, 1996.
R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1–11, 1995.
Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. ICALP'98, LNCS, 1998.
L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engin., 3:125–143, 1977.
D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. POPL'97, 1997.
D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. ICALP'81, vol. 115 of LNCS, pp 264–277, 1981.
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.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. CAV'89, vol. 407 of LNCS, pp 151–165, 1989.
A.P. Sistla and S.M. German. Reasoning about systems with many processes. J. ACM, 39:675–735, 1992.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. CAV'89, vol. 407 of LNCS, pp 68–80, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kesten, Y., Pnueli, A. (1998). Modularization and abstraction: The keys to practical formal verification. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055757
Download citation
DOI: https://doi.org/10.1007/BFb0055757
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive