Model checking and modular verification

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. Additionally, 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.

REFERENCES

• 1: BEN-ARI, M., MANNA, Z., AND PNUELI, A. 1983. The temporal logic of branching time. Acta Informatica 20, 207-226.
• 2: BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL, D. L., AND HWANG, J. 1990. Symbolic model checking: 102o states and beyond. In Proceedings of the 5th Annual Symposium on Logic ~n Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.
• 3: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 4: E. M. Clarke , I. A. Browne , R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of &ohgr;-automata, Proceedings of the fifteenth colloquium on CAAP'90, p.103-116, May 1990, Copenhagen, Denmark
• 5: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 6: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 7: CLARKE, E. M., LONG, D. E., AND MCMILLAN, K. L 1989b. A language for compositional specification and verification of finite state hardware controllers. In Proceedtngs of the 9th International Symposzum on Computer Hardware Descmpt~on Languages and thezr Appltcations. North-Holland, Amsterdam.
• 8: R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, v.27 n.9, p.725-747, Sep. 1990
• 9: CLEAVELAND, R., AND STEFFEN, B. 1990. When is "partial" adequate. A logic-based proof technique using partial specifications. In Proceedings of the 5th Annual Sympostum on Logzc in Computer Sctence. IEEE Computer Society Press, Los Alamitos, Calif.
• 10: R. Cleaveland , J. Parrow , B. Steffen, The concurrency workbench, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.24-37, February 1990, Grenoble, France
• 11: Olivier Coudert , Jean Christophe Madre , Christian Berthet, Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.23-32, June 18-21, 1990
• 12: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
• 13: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 14: EMERSON, E. A., AND LEI, C.-L. 1986. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the 1st Annual Sympostum on Logic ~n Computer Science IEEE Computer Society Press, Los Alamitos, Calif.
• 15: Susanne Graf , Bernhard Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.186-196, June 18-21, 1990
• 16: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 17: B. Josko, Verifying the correctness of AADL modules using model checking, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.386-400, May 1990, Mook, The Netherlands
• 18: R. P. Kurshan, Analysis of discrete event coordination, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.414-453, May 1990, Mook, The Netherlands
• 19: R. P. Kurshan , K. McMillan, A structural induction theorem for processes, Proceedings of the eighth annual ACM Symposium on Principles of distributed computing, p.239-247, June 1989, Edmonton, Alberta, Canada [doi>10.1145/72981.72998]
• 20: Kim Guldstrand Larsen, The expressive power of implicit specifications, Proceedings of the 18th international colloquium on Automata, languages and programming, p.204-216, June 1991, Madrid, Spain
• 21: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 22: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 23: MILNER, R. 1971. An algebraic definition of simulation between programs. In Proceedtngs of the 2nd International Joint Conference on Artificial Intelhgence (Sept.).
• 24: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 25: PNUELI, A., AND SHERMAN, R. 1981 Semantic tableau for temporal logic. Tech. Rep. CS81-21, The Weizmann Institute, Israel.
• 26: Z. Shtadler , O. Grumberg, Network grammars, communication behaviors and automatic verification, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.151-165, February 1990, Grenoble, France
• 27: Gil Shurek , Orna Grumberg, The Modular Framework of Computer-Aided Verification, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.214-223, June 18-21, 1990
• 28: Colin Stirling , David Walker, Local Model Checking in the Modal Mu-Calculus, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming, p.369-383, March 13-17, 1989
• 29: WALKER, D. 1988. Bisimulations and divergence. In Proceedings of the 3rd Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.
• 30: Glynn Winskel, A note on model checking the model &ngr;-calculus, Selected papers of the 16th international colloquium on Automata, languages, and programming, p.157-167, June 1991, Stresa, Italy
• 31: WOLPER, P. 1983. Temporal logic can be more expressive. Infi Contr. 56, 1/2 (Jan./Feb.), 72-99.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE); Decision tables

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Relations between models

General Terms:
Algorithms, Design, Languages, Theory, Verification

Keywords:
CTL, Moore machines, computer-aided verification, formal verification, model checking, temporal logics