Model Construction for Finite-state Verification
ProjectTitleLine: Model Construction for Finite-state Verification :Application of Abstract Interpretation and Partial Evaluation Techniques
Period: 01 April 1998 through 1 April 2000
Grant Number: NASA NAG-2-1209
Investigators: Matthew Dwyer, John Hatcliff, David A. Schmidt
InstitutionLine: Kansas State University
POC: schmidt@cis.ksu.edu
Objective:
In this project we investigate solutions of three fundamental problems hindering the application of finite-state verification (``model checking'') techniques to software:
- the derivation of sound, finite-state models for distributed software systems
- the automation of the finite-model construction technique
- the limitation of the cardinality of the constructed models to a tractable size
We attack these problems by employing new technology based on the maturing formal-methods techniques of abstract interpretation and partial evaluation:
- Abstract interpretation, a technique for symbolically executing programs, will be employed to define a hierarchy of semantically correct ``property sets'' that can be used with symbolic execution. Crucially, the result of a symbolic execution with abstract interpretation is a finite-state model that is a safe abstraction of the state space of the original program.
- Partial evaluation, an automated program simplification/transformation methodology, will be used as the ``engine'' to drive the abstract interpretation. Partial evaluation provides the needed automation, because it is general purpose and robust---it can be applied to any abstract interpretation and any source program, and it will generate automatically the desired finite-state models.
- Finally, the interaction of abstract interpretation and partial evaluation generates a synergy otherwise absent---the cardinality of the automatically generated finite-state models can be controlled by tuning partial evaluation's specialization and inlining algorithms to interact optimally with the choice of property sets within the abstract interpretation.
Our methodology liberates the software designer from the burden of designing by hand ad-hoc, potentially incorrect, abstract models of software systems. It also allows the separation-of-concerns of model creation from model checking, meaning that the optimal model checker can be selected for checking a specific class of models.
In addition, the robustness of partial evaluation technology allows it to be applied to modular or ``open'' programs, advancing the frontier of compositional model checking.
We also envisage that our integration of abstract interpretation and partial evaluation machinery will let us undertake serious application of radical state-space reduction techniques based on semantically pseudo-safe abstractions, where symbolic execution undertaken by abstract interpretation might be semantically unsound for some program properties, but it is semantically sound for the correctness properties of interest to the software designer.
Project Reports
For technical details see the Bandera Project.
- Project Quad-Chart (July, 1998)
- Project Progress Report (July, 1998)
- PI Meeting Presentation (Nov, 1998)
- Project Progress Report (Nov, 1998)
- Project Progress Report (Feb, 1999)
- Project Progress Report (April, 1999)
- Project Progress Report (June, 1999)
- Here are links to our talks at the May PI meeting on Bandera and the Verification and Validation Group Summary.
Project Publications
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
- Schmidt, D.A. Programming Principles in Java. Scott-Jones Press, 491pp., (to appear 2000). (electronic versions of this book are not available).
- George S. Avrunin, James C. Corbett and Matthew B. Dwyer, Benchmarking Finite-state Verifiers, International Journal on Software Tools for Technology Transfer (to appear).
- John Hatcliff, Matthew B. Dwyer and Hongjun Zheng, Slicing Software for Model Construction, Journal of Higher-Order and Symbolic Computation (to appear).
- Matthew B. Dwyer and Corina S. Pasareanu, Model Checking Generic Container Implementations, Proceedings of the 1st Dagstuhl Symposium on Generic Programming, LNCS (to appear).
- M"uller-Olm, M., Schmidt, D.A. and Steffen, B. Model checking: a tutorial introduction. Proc. 6th Static Analysis Symposium, G. File and A. Cortesi, eds., LNCS 1694, Springer-Verlag, pp. 330-354. Here are the slides from the presentation (contains additional material).
- John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hongjun Zheng, A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, Proceedings of the Static Analysis Symposium, LNCS 1694, Springer-Verlag, Sept, 1999.
- Corina S. Pasareanu, Matthew B. Dwyer and Michael Huth, Assume-Guarantee Model Checking of Software : A Comparative Case Study, Theoretical and Practical Aspects of SPIN Model Checking, LNCS 1680, Springer-Verlag, Sept, 1999.
- Matthew B. Dwyer, George S. Avrunin, and James C. Corbett, Patterns in Property Specifications for Finite-state Verification, Proceedings of the 21st International Conference on Software Engineering, May, 1999.
- Matthew B. Dwyer and John Hatcliff, Slicing Software for Model Construction, Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'99), January, 1999.
- Schmidt, D.A. A Return to Elegance: The Reapplication of Declarative Notation to Software Design. Invited position paper, Proc. First Workshop in Practical Aspects of Declarative Languages, San Antonio, TX, Janaury 1999, G. Gupta, ed., Springer LNCS 1551.
- Matthew B. Dwyer, John Hatcliff, and Dave Schmidt, Bandera: Tools for Automated Reasoning about Software System Behaviour, ERCIM News, No. 36, January, 1999.
- Matthew B. Dwyer and Corina S. Pasareanu. Filter-based Model Checking of Partial Systems, in the Proceedings of the ACM SIGSOFT Sixth International Symposium on the Foundation of Software Engineering, November, 1998.
- Schmidt, D.A. and Steffen, B. Data-flow analysis as model checking of abstract interpretations. Proc. 5th Static Analysis Symposium, G. Levi. ed., Pisa, September, 1998. LNCS 1503, Springer-Verlag.
- John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and David Schmidt. Staging Static Analyses Using Abstraction-based Program Specialization , Proceedings of Principles of Declarative Programming: 10th International Symposium (PLILP'98), LNCS 1490, Springer-Verlag, September, 1998.
Related Links
- The SAnToS Laboratory at Kansas State University
- NASA
- Automated Software Engineering Group at NASA Ames Research Center.
- Computing and Information Sciences Department home page