NASA Logo, National Aeronautics and Space Administration

Propel: Property Checking for C++

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

Publications

Overview "Propel: Tools and Methods for Practical Software Model Checking," Masoud Mansouri-Samani, Peter Mehlitz, Lawrence Markosian, Owen O'Malley, Dale Martin, Lantz Moore, John Penix, Willem Visser. Workshop on Model Checking for Software Intensive Systems at Dependable Systems and Networks Conference, June 2003.
[paper (PDF, 69K)]



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.

Reviewed 2012



Researchers

Other Info

Publications

First Gov logo
NASA Logo - nasa.gov