|Project Title:||Model Construction for Finite-state Verification: Application of Abstract Interpretation and Partial Evaluation Techniques.|
|Organization:||Kansas State University|
|Contract Number:||NASA NAG2-1209|
|Start Date:||01 APR 1998|
|End Date:||31 MAR 2000|
The project aims to apply finite-state verification technology, currently used for hardware systems, to modern concurrent embedded component-based software systems. The resulting tools will help engineers detect subtle faults, otherwise undetectable by testing, in long-lived mission-critical embedded software systems prior to deployment. To build these tools, three fundamental challenges to existing verification technology will be addressed: (i) the derivation of sound, finite-state models for software systems; (ii) the automation of the finite-model construction process; and (iii) the limitation of the constructed models to a tractable size.
Previous attempts to adapt model-checking technology to software systems have been hampered by the inability to automatically synthesize tractably sized, guaranteed-semantically-safe models. The project attacks these difficulties with novel technology based on the maturing formal-methods techniques of abstract interpretation and partial evaluation.
Abstract interpretation is a technique for symbolically executing programs; it 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 guaranteed-safe abstraction of the state space of the original program.
Partial evaluation is an automated program simplification/transformation methodology; it will be used as the ``engine'' to drive the abstract interpretation. Partial evaluation is particularly attractive 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.
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.
A major payoff of this methodology is that it 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 component-based or ``open'' systems, advancing the frontiers of compositional model checking.
It is hoped that the integration of abstract interpretation and partial evaluation machinery will let software engineers employ 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 is semantically sound for the correctness properties of interest to the software designer.
A theory of abstraction-based partial evaluation (ABPE) has been formalized. Based on the formalization, tool prototypes for an Ada subset were constructed.
The tool prototypes were used to automatically construct models for nontrivial case studies of reactive software components, most notably an Ada generic program that organizes replicated worker computations (that is, parallel computations where each sub-problem is an instance of the same computation) in which the programmer interface hides management of parallelism, sub-problem scheduling, and termination detection.
The automatically constructed models were verified with the SPIN model checker and the FLAVERS analysis system. Such examples were previously modelled and verified only after extensive, tedious, and error-prone transformations were performed by hand.
The work with Ada software will continue, but the shift in commercial and academic research communities towards Java for concurrent and parallel applications dictates that the tools be targeted towards both Ada and Java. The near-term plan includes three components:
Adaptation and development of an abstraction-based partial evaluation toolset for Java byte codes. This will give a source-language-independent framework, facilitate integration of existing and forthcoming tools for byte-code analysis, and provide a platform for verifying mobile code and dynamically reconfigurable systems. The tools will be targeted to applications written in Java and Ada-95. (Ada-95 can be compiled to byte-code using Intermetrics' Ada-Magic system.)
Evaluation of the tools' effectiveness on existing applications and test cases from the finite-state verification community.
Based on feedback from the evaluation stage, refinement of the toolset and planning for transition to various technology partners (discussed below). In particular, NASA's Automated Software Engineering (ASE) is targeted as an early adopter of the technology for analyzing deep-space probe software.
Our project has begun cooperation with other ongoing research projects to insure that the tools integrate properly with tools produced elsewhere. Since the project is a new start, the plan that follows is preliminary:
Two projects, an NSF Experimental Software Systems project and a DARPA/EDCS project, centered at the University of Massachusetts, are devoted to the development of high-quality translators into the input languages of existing model checking tools. Our project's toolset will bridge the gap from high-level program source to the input of their low-level translators.
NASA Ames ASE has been identified as an interested consumer of a model construction toolset for Java programs targeted at SPIN. Our tools form a crucial component of this toolset and we plan to transfer our tools to this group.
An ongoing DARPA-funded project at the University of Kansas is developing technology for generating dynamically reconfigurable digital radios on field-programmable gate-arrays (FPGAs) from specifications written a high-level domain-specific programming language. In collaboration with researchers on this project, our tools will be targeted to their domain-specific language, thereby enabling model checking of correctness properties of evolving circuits.