Symbolic model checking of declarative relational models

ABSTRACT

This paper explores the idea of augmenting traditional model checkers with the expressiveness of a declarative, relational language. The goal is to enable programmers to write very intuitive and compact specifications, in order to allow the automatic verification of more complicated software systems. The key idea is that many structural operations (common in object-oriented programs) can be easily described using relations and relational operators, while other operations are best described using the primitive data types and their operations (such as simple arithmetic operations on numbers). By allowing a mixture of both, and by allowing parts of the model to be described declaratively rather than imperatively, the programmer has the freedom to model each part of the system differently, using the most intuitive and simple constructs. We built a BDD-based model checker for the language, and successfully verified a straightforward model of the dependency algorithm in Apache Ant for up to 5 nodes.

REFERENCES

• 1: A. Tarski. A lattice-theoretical fixpoint theorem and its applications. In Pacific Journal of Mathematics 5, pages 285--309.
• 2: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 3: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 4: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 5: David L. Dill, The Murphi Verification System, Proceedings of the 8th International Conference on Computer Aided Verification, p.390-393, August 03, 1996
• 6: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 7: 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]
• 8: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 9: Jonathan Edwards , Daniel Jackson , Emina Torlak, A type system for object models, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 10: Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
• 11: J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, 1990.
• 12: Ken Arnold and James Gosling. The Java Programming Language. Addison-Wesley, 1996.
• 13: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 14: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 15: A. Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symp. Foundations of Computer Science, 1977.
• 16: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 17: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 18: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
computation tree logic, software model checking