Verifying systems with integer constraints and Boolean predicates: a composite approach

ABSTRACT

Symbolic mode, checking has proved highly successful for large finite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to systems with an infinite number of states --- even those with a single unbounded integer.Alternatively, we recently proposed a model checker for integer-based systems that uses Presburger constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of Boolean and (unordered) enumerated types --- which possess no natural mapping to the Euclidean coordinate space.In this paper we describe a model checker which combines the strengths of both approaches. We use a composite model, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. We demonstrate our technique's effectiveness on a nontrivial requirements specification, which includes a mixture of Booleans, integers and enumerated types.

REFERENCES

• 1: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 2: Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996 [doi>10.1109/32.489079]
• 3: Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.156-166, October 16-18, 1996, San Francisco, California, United States
• 4: Joanne M. Atlee , Michael A. Buckley, A logic-model semantics for SCR software requirements, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.280-292, January 08-10, 1996, San Diego, California, United States
• 5: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305]
• 6: André Arnold , John Plaice, Finite transition systems: semantics of communicating systems, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 7: R. Bhaxadwaj, and C. Heitmeyer.' Verifying SCR requirements specifications using state exploration. In Proceedings of First A CM $IGPLAN Workshop on A utomatic Analysis of Software, Jan 1997.
• 8: Bernard Boigelot , Patrice Godefroid, Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract), Proceedings of the 8th International Conference on Computer Aided Verification, p.1-12, August 03, 1996
• 9: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 10: Randal E. Bryant , Yirng-An Chen, Verification of arithmetic circuits with binary moment diagrams, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.535-541, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217583]
• 11: Tevfik Bultan , Richard Gerber , William Pugh, Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic, Proceedings of the 9th International Conference on Computer Aided Verification, p.400-411, June 22-25, 1997
• 12: J. R. Butch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 102~ states and beyond. In Proc. of the 5th Annual IEEE Sym. posium on Logic in Computer Science, pages 428-439, 1990.
• 13: William Chan , Richard Anderson , Paul Beame , David Notkin, Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints, Proceedings of the 9th International Conference on Computer Aided Verification, p.316-327, June 22-25, 1997
• 14: 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]
• 15: Edmund Clarke , Xudong Zhao, Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits, Carnegie Mellon University, Pittsburgh, PA, 1995
• 16: P.-J. Courtois , D. L. Parnas, Documentation for safety critical software, Proceedings of the 15th international conference on Software Engineering, p.315-323, May 17-21, 1993, Baltimore, Maryland, United States
• 17: Patrice Godefroid , David E. Long, Symbolic Protocol Verification with Queue BDDs, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.198, July 27-30, 1996
• 18: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 19: W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman and D. Wonnacott. The Omega Library (version 1.00) interface guide. Available at <http://www.cs.umd.edu/projects/omega>.
• 20: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 21: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 22: A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993 [doi>10.1145/158439.158441]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

General Terms:
Experimentation, Languages, Verification