Using predicate abstraction to reduce object-oriented programs for model checking

ABSTRACT

While it is becoming more common to see model checking applied to software requirements specifications, it is seldom applied to software implementations. The Automated Software Engineering group at NASA Ames is currently investigating the use of model checking for actual source code, with the eventual goal of allowing software developers to augment traditional testing with model checking. Because model checking suffers from the state-explosion problem, one of the main hurdles for program model checking is reducing the size of the program. In this paper we investigate the use of abstraction techniques to reduce the state-space of a real-time operating system kernel written in C++. We show how informal abstraction arguments could be formalized and improved upon within the framework of predicate abstraction, a technique based on abstract interpretation. We introduce some extensions to predicate abstraction that all allow it to be used within the class-instance framework of object-oriented languages. We then demonstrate how these extensions were integrated into an abstraction tool that performs automated predicate abstraction of Java programs.

REFERENCES

• 1: 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
• 2: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 3: 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
• 4: William Chan , Richard J. Anderson , Paul Beame , David H. Jones , David Notkin , William E. Warner, Decoupling synchronization from local control for efficient symbolic model checking of statecharts, Proceedings of the 21st international conference on Software engineering, p.142-151, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302460]
• 5: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 6: Michael Colón , Tomás E. Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, Proceedings of the 10th International Conference on Computer Aided Verification, p.293-304, June 28-July 02, 1998
• 7: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 8: P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 4(2):511-547, August 1992.
• 9: Zhe Dang , Richard A. Kemmerer, Using the ASTRAL model checker to analyze mobile IP, Proceedings of the 21st international conference on Software engineering, p.132-141, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302459]
• 10: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 11: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 12: K. Havelund and T. Pressburger. Model checking java programs using java pathfinder, International Journal on Software Tools for Technology Transfer, 1999.
• 13: Klaus Havelund, Michael Lowry, SeungJoon Park, Charles Pecheur, John Penix, Willem Visser, and Jon L. White. Formal analysis of the remot agent before mid after flight. In Lfm 2000: Fifth NASA Langley Formal Methods Workshop, 2000.
• 14: 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]
• 15: Gerard J. Holzmann , Margaret H. Smith, A practical method for verifying event-driven software, Proceedings of the 21st international conference on Software engineering, p.597-607, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302710]
• 16: Gleb Naumovich , George S. Avrunin , Lori A. Clarke, Data flow analysis for checking properties of concurrent Java programs, Proceedings of the 21st international conference on Software engineering, p.399-410, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302663]
• 17: B. Pell, E. Gat, R. Keesing, N. Muscettola, mid B. Smith. Plan Execution for Autonomous Spacecrafts. In Proceedings of the International Joint Conference on Artificial Intelbigence, August 1997. Nagoya, Japan.
• 18: John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337364]
• 19: Hassen Saïdi, Modular and Incremental Analysis of Concurrent Software Systems, Proceedings of the 14th IEEE international conference on Automated software engineering, p.92, October 12-15, 1999
• 20: Hassen Saïdi , Natarajan Shankar, Abstract and Model Check While You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, p.443-454, July 06-10, 1999
• 21: David A. Schmidt , Bernhard Steffen, Program Analysis as Model Checking of Abstract Interpretations, Proceedings of the 5th International Symposium on Static Analysis, p.351-380, September 14-16, 1998

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

General Terms:
Design, Measurement, Performance, Reliability, Theory, Verification

Keywords:
browsing