IV&V Facility Research Program Results and SARP Results  

Advanced Search
Software Safety < Results Home

Click here to complete a short survey. The results of this survey will be used to help us improve the research program and this website.

Click here to view research projects that had new research results added in the last 90 days.
Formal Methods Analysis Framework
Point of Contact David Owen
David.R.Owen@ivv.nasa.gov
Dates June 2006 - December 2006
Problem The Shuttle abort control sequencer had the highest density of severity 1 discrepancies, the Space Station vehicle power retry design was untestable, and in-flight concurrency issues have been experienced with both the Shuttle GPS integration and the control handoff between the Space Station CCS and NCS computers. This software was highly complex and presented a V&V challenge due to the large number of potential combinations of internal and environmental operational states.

Automated formal methods tools are effective for testing these types of software but only within small problem sets and abstract models. We intend to apply formal methods in a practical, scalable way to larger and more complex problem sets and add verification and test automation in a simulation environment. Specifically, we plan to integrate Lurch, a tool for detecting errors in formal models, as well as TAR3, a lightweight machine learning tool, with the Reconfigurable Environment for Analysis and Test of Software Systems (REATSS) currently being developed for the IV&V Facility. The end result will be a framework through which an analyst can access model checking functionality (through Lurch), machine learning functionality (through TAR3), and simulation functionality (through REATSS)?all from the same interface. This set of tools, the Formal Methods Analysis Framework (FMAF), will enable IV&V analysts to perform tests and evaluations that would otherwise not be possible. Specifically, users of the FMAF will be able to:
  1. Run a batch of simulations, using automated techniques from formal methods to check software logic for violations of specified safety or liveness properties, or deadlocks.
  2. For that same batch of simulations, or other simulations done manually, apply automated techniques from machine learning to summarize the large amounts of data produced by the simulator?to produce, for example, general testability and coverage data to help determine the effectiveness of testing methods represented by the simulation data.
In summary, the FMAF project will arm analysts with advanced tools developed by the NASA IV&V Facility to perform V&V tasks that could otherwise not be performed on critical areas of spacecraft software.
Objective The objective of this initiative is to create a practical, user-friendly framework for applying formal methods in an efficient, scalable way to NASA IV&V projects. Our work will be performed in three phases. The objective of Phase 1 is to develop a detailed plan for the initiative, including a concept of operations, requirements and a conceptual design. The objective of Phase 2 is to implement a proof of concept based on that design. The objective of Phase 3 is to develop a user-friendly FMAF accessible to IV&V analysts and to demonstrate its use on a NASA IV&V project.
Results SAS 06 Executive Presentation.ppt
SAS 06 Technical Presentation.ppt
FMAF Concept of Operations.doc
Conceptual Design.doc
Plan for Phases 2 and 3.doc
Keywords formal methods, model checking, data mining, machine learning, treatment learning, simulation, automated testing, tool framework
Categories Software Safety
Domain-Specific Analysis
Dynamic Analysis
Formal Methods
Test Analysis


Curator: Josh Stonestreet
NASA Official: Lisa Montgomery
 NASA Insignia NASA Privacy, Security, Notices