NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Propel: Tools and Methods for Practical Source Code Model CheckingThe work reported here is an overview and snapshot of a project to develop practical model checking tools for in-the-loop verification of NASA s mission-critical, multithreaded programs in Java and C++. Our strategy is to develop and evaluate both a design concept that enables the application of model checking technology to C++ and Java, and a model checking toolset for C++ and Java. The design concept and the associated model checking toolset is called Propel. It builds upon the Java PathFinder (JPF) tool, an explicit state model checker for Java applications developed by the Automated Software Engineering group at NASA Ames Research Center. The design concept that we are developing is Design for Verification (D4V). This is an adaption of existing best design practices that has the desired side-effect of enhancing verifiability by improving modularity and decreasing accidental complexity. D4V, we believe, enhances the applicability of a variety of V&V approaches; we are developing the concept in the context of model checking. The model checking toolset, Propel, is based on extending JPF to handle C++. Our principal tasks in developing the toolset are to build a translator from C++ to Java, productize JPF, and evaluate the toolset in the context of D4V. Through all these tasks we are testing Propel capabilities on customer applications.
Document ID
20030054563
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
Mansouri-Samani, Massoud
(Computer Sciences Corp. United States)
Mehlitz, Peter
(Computer Sciences Corp. United States)
Markosian, Lawrence
(QSS Group, Inc. United States)
OMalley, Owen
(QSS Group, Inc. United States)
Martin, Dale
(Clifton Labs., Inc. United States)
Moore, Lantz
(Clifton Labs., Inc. United States)
Penix, John
(NASA Ames Research Center Moffett Field, CA, United States)
Visser, Willem
(Research Inst. for Advanced Computer Science Moffett Field, CA, United States)
Date Acquired
August 21, 2013
Publication Date
April 8, 2003
Subject Category
Computer Programming And Software
Meeting Information
Meeting: Workshop on Dependable Software-Intensive Systems
Location: San Francisco, CA
Country: United States
Start Date: June 22, 2003
End Date: June 25, 2003
Funding Number(s)
CONTRACT_GRANT: NAS2-00065
Distribution Limits
Public
Copyright
Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available