We are developing a model checking toolset and methodologies to enable practical application of model checking to C++. The toolset builds upon Java PathFinder (JPF), an explicit-state model checker for Java, by adding extensions to support C++. The approach involves building a translator from C++ to Java, and re-architecting many aspects of JPF to increase extensibility and observability. The translator is implemented with an Edison Design Group-based C++ parser, which we extended to create an XML-based abstract syntax tree (AST). Various tree-based transformations to replace the non-Java-like parts of C++ with Java equivalents are then applied to the AST and, finally, Java code is published from the AST.
As part of Propel, we are developing a "Design for Verification" methodology that explicitly adds V&V goals to the design phase. The objective is to turn V&V into a development co-process by mapping key system properties to dedicated, separately checkable design components. This is achieved mainly by using domain-specific design pattern systems, where each pattern instance has its own set of tool-supported usage checks and guarantees. These, in turn, are used to identify suitable pattern candidates based on the system specification
C++ Model Checking via JPF "C++ Design and Usage Guidelines for Program Model Checking with Propel," Peter Mehlitz and Owen O'Malley, Ames TR, March 2003.
Design for Verification
"Design for Verification: Using Design Patterns to Build Reliable Systems,"
Peter C. Mehlitz and John Penix, Workshop on Component-Based Software Engineering
at International Conference on Software Engineering, May 2003.
[paper (PDF, 121K)]
"Design for Verification with Dynamic Assertions", Peter C. Mehlitz, NASA Ames Technical Report, July 2003. PDF
Using Model Checking to Improve Testing "A Test Data Selection Framework for Model Checking," John Penix and Owen O'Malley, Peter Mehlitz.
Technology Transfer Issues
"Technology Transfer Challenges for High-Assurance Software Engineering
Tools," John Penix and Lawrence Markosian, Workshop on Software Engineering
for High Assurance Systems: Process, Product, and Profiling, at International
Conference on Software Engineering, May 2003.
[paper (PDF, 101K)]
"Hosted Services for Advanced V&V Technologies: An Approach to Achieving
Adoption withou the Woes of Usage," Lawrence Z. Markosian, Owen O'Malley,
John Penix and William Brew, Position Paper for the ICSE Workshop on Adoption-Centric
Software Engineering, May 2003.
[paper (PDF, 78K)]
"Verification of g-Limit Using the PolySpace Verifier," Masoud Mansouri-Samani, Owen O'Malley, Lawrence Markosian and C. Scott Akridge, Ames TR, April 2003.