Compositional verification by model checking for counter-examples

ABSTRACT

Many concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using model checking. In this approach an abstract, finite-state model of the system is constructed; then an automatic check is made to ensure that the requirements are satisfied by the model. In practice, however, this method is limited by the state space explosion problem.We have developed a compositional method that directly addresses this problem in the context of multi-tasking programs. Our solution depends on three key space-saving ingredients: (1) checking for counter-examples, which leads to simpler search algorithms; (2) automatic extraction of interfaces, which allows a refinement of the finite model --- even before its communicating partners have been compiled; and (3) using propositional "strengthening assertions" for the sole purpose of reducing state space.In this paper we present our compositional approach, and describe the software tools that support it.

REFERENCES

• 1: Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , Pei-Hsin Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, Hybrid Systems, p.209-229, January 1993
• 2: J. 1%. Burch, E. M. Clarke, K. L. McMillan, D. L Dill, and L H Hwang. Symbolic model checking: 1020 states and beyond. Proceedings of the F~fth Annual Sympos,um on Logzc ,n Computer Science, 428-439, 1990.
• 3: Thomas R. Shiple , Massimiliano Chiodo , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Automatic Reduction in CTL Compositional Model Checking, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.234-247, June 29-July 01, 1992
• 4: 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]
• 5: S. C. Cheung , J. Kramer, Enhancing compositional reachability analysis with context constraints, Proceedings of the 1st ACM SIGSOFT symposium on Foundations of software engineering, p.115-125, December 08-10, 1993, Los Angeles, California, United States
• 6: R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, v.27 n.9, p.725-747, Sep. 1990
• 7: 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
• 8: 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
• 9: 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]
• 10: E. A. Emerson and C Lei. Efficient model checking m fragments of the propositional mu-calculus. Proceedings of Symposium on Log,c ~n Computer Science, 267-278, 1986
• 11: J. Fischer and R Gerber. Compositional Model Checking of Ada Tasking Programs Proceedings COMPASS'9~i. 1994.
• 12: Nicolas Halbwachs, Delay Analysis in Synchronous Programs, Proceedings of the 5th International Conference on Computer Aided Verification, p.333-346, June 28-July 01, 1993
• 13: R. J. van Glabbeek, The linear time-branching time spectrum (extended abstract), Proceedings on Theories of concurrency : unification and extension: unification and extension, p.278-297, September 1990, Amsterdam, The Netherlands
• 14: Richard Gerber , Insup Lee, Guest A Layered Approach to Automating the Verification of Real-Time Systems, IEEE Transactions on Software Engineering, v.18 n.9, p.768-784, September 1992 [doi>10.1109/32.159838]
• 15: O. Lichtenstein and A. PnueIi Checking that finite state concurrent programs satmfy their hnear specifications. 1984.
• 16: J. S. Ostroff. Survey of formal methods for the spec~ficat,on and design of real-t,me systems. Draft for IEEE Press book "Tutorial on Specification of Time", 1992.
• 17: C. Stirling , D. Walker, CCS, liveness, and local model checking in the linear time mu-calculus, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.166-178, February 1990, Grenoble, France
• 18: Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Modeling techniques

General Terms:
Design, Theory, Verification