Abstract
We describe a framework for compositional verification of finite state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition; and a preorder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the logic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee style reasoning within this framework. In addition, we demonstrate efficient methods for model checking in the logic and for checking the preorder in several special cases. We have implemented a system based on these methods, and we use it to give a compositional verification of a CPU controller.
This research was sponsored in part by the Avionics Laboratory, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, Ohio 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation under Contract No. CCR-9005992 and in part by the U.S.-Israeli Binational Science Foundation.
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. government.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1990.
E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A unified approach for showing language containment and equivalence between various types of ω-automata. In A. Arnold and N. D. Jones, editors, Proceedings of the 15th Colloquium on Trees in Algebra and Programming, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, May 1990.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1989.
E. M. Clarke, D. E. Long, and K. L. McMillan. A language for compositional specification and verification of finite state hardware controllers. In J. A. Darringer and F. J. Rammig, editors, Proceedings of the Ninth International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, June 1989.
R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27:725–747, 1990.
O. Coudert, C. Berthet, and J. C. Madre. Verifying temporal properties of sequential machines without building their state diagrams. In Kurshan and Clarke [16].
J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors. Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science. Springer-Verlag, May 1989.
D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations, MIT Press, 1989.
E. A. Emerson and J. Y. Halpern. “Sometimes” and “Not Never” revisited: On branching time versus linear time. Journal of the ACM, 33:151–178, 1986.
E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mucalculus. In Proceedings of the Second Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986.
S. Graf and B. Steffen. Compositional minimization of finite state processes. In Kurshan and Clarke [16].
J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.
B. Josko. Verifying the correctness of AADL-modules using model checking. In de Bakker et al. [8].
R. P. Kurshan. Analysis of discrete event coordination. In de Bakker et al. [8].
R. P. Kurshan and E. M. Clarke, editors. Proceedings of the 1990 Workshop on Computer-Aided Verification, June 1990.
R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing. ACM Press, August 1989.
K. G. Larsen. The expressive power of implicit specifications. To appear in Proceedings of the Eighteenth International Colloquium on Automata, Languages, and Programming.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, January 1985.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
A. Pnueli. In transition for global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume 13 of NATO ASI series. Series F, Computer and system sciences. Springer-Verlag, 1984.
Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In J. Sifakis, editor, Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989.
G. Shurek and O. Grumberg. The modular framework of computer-aided verification: Motivation, solutions and evaluation criteria. In Kurshan and Clarke [16].
C. Stirling and D. J. Walker. Local model checking in the modal mu-calculus. In J. Diaz and F. Orejas, editors, Proceedings of the 1989 International Joint Conference on Theory and Practice of Software Development, volume 351–352 of Lecture Notes in Computer Science. Springer-Verlag, March 1989.
D. Walker. Bisimulations and divergence. In Proceedings of the Third Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1988.
G. Winskel. Compositional checking of validity on finite state processes. Draft copy.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grumberg, O., Long, D.E. (1991). Model checking and modular verification. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_93
Download citation
DOI: https://doi.org/10.1007/3-540-54430-5_93
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54430-2
Online ISBN: 978-3-540-38357-4
eBook Packages: Springer Book Archive