Model-Based System Engineering is becoming widely adopted at JPL and in industry because model-centric systems introduce improved methods of system engineering. As systems with ever-increasing complexity are developed at JPL, model-centric engineering be comes essential for design, test, and validation. Validation of FP designs is historically problematic, with many examples of inadequate resources (people, time, and budget) and/or unexpected problems. Many factors contribute to these issues, but the problem can be traced to a lack of appreciation of system complexity. When considering a system, there are significantly more ways the system can fail (contingency paths) than ways it can succeed (nominal paths). As NASA continues to develop more complex and capable spacecraft, the behavior state space will increase, stressing the ability of teams to properly understand system behavior.
This technology provides the ability to implement fault management logical design into a SysML (System Modeling Language) behavior model using Statecharts; exploit multi-fault, multi-response fault injection test simulations; and formally validate the logical design of the fault management system against correctness properties via model checking.
To implement model checking, the SysML model is transformed to Java and then executed in the model checker, Java Pathfinder (JPF). The model checker compares properties to check (logical assertions) against the modeled behavior as it explores all possible paths within the state space of the model. If counterexamples of the properties to check are found, the model checker generates an error trace report, documenting the set of scenarios that result in each failed assertion.
This work is novel because the defined modeling framework allows the same behavior model to be both executable and formally checkable. The advantages of modeling fault protection logical design, executing the model, and validating via a model checker are:
- Designing logical behavior of a system in a model is less prone to human error.
- Simulating multi-fault, multi-response fault injection tests in the model increases the test domain and verifies system behavior.
- Auto-generation of event reports for fault injection tests provides a useful product for understanding system behavior (designing and testing).
- Validating the logical design of the system against domain-specific constraints.
- Significantly reducing the effort needed to develop related artifacts from a model that has been formally validated, including design documentation (dictionaries), flight software, and test procedure outlines.
The ability to test and formally validate fault protection logical design models expands the test domain and could lower cost, shorten schedules, reduce risk for flight projects, and enable better understanding of complex systems. As SysML continues to become prevalent on missions and in system engineering, the use of this technology may become standard practice.
This work was done by John C. Day and Corrina L. Gibson of Caltech, and Robert Karban and Luigi Andolfato of the European Southern Observator y for NASA’s Jet Propulsion Laboratory.
The software used in this innovation is available for commercial licensing. Please contact Dan Broderick at
This Brief includes a Technical Support Package (TSP).
Formal Validation of Model-Based Fault Management Design Solutions
(reference NPO-49337) is currently available for download from the TSP library.
Don't have an account?
Overview
The document is a Technical Support Package from NASA's Jet Propulsion Laboratory (JPL) detailing the "Formal Validation of Model-Based Fault Management Design Solutions," identified by NASA Tech Brief NPO-49337. It outlines the research and methodologies developed to enhance fault management systems in autonomous spacecraft.
The primary focus of the document is on the formal validation processes that ensure the reliability and effectiveness of fault management designs. This is crucial for missions where unexpected conditions can arise, potentially jeopardizing the success of the mission. The research emphasizes the need for robust fault protection systems that can autonomously detect and respond to anomalies, thereby maintaining operational integrity.
Key contributors to this research include Corrina Gibson, Robert Karban, Luigi Andolfato, and John Day, among others, all affiliated with JPL and the European Southern Observatory (ESO). Their collaborative efforts aim to create executable and checkable fault management models that can be rigorously validated to ensure they perform as intended under various scenarios.
The document also references additional resources and contributions, including presentations made at the Conference on Systems Engineering Research (CSER) in 2014, where findings related to fault management were shared with the broader engineering community. The work is part of NASA's Commercial Technology Program, which seeks to disseminate aerospace-related developments that have potential applications beyond space exploration.
Furthermore, the document provides contact information for the Innovative Technology Assets Management office at JPL, encouraging further inquiries into the research and technology discussed. It also includes a disclaimer regarding the use of the information contained within, clarifying that the U.S. Government does not assume liability for its application.
In summary, this Technical Support Package serves as a comprehensive overview of the advancements in formal validation techniques for fault management systems, highlighting the importance of these systems in ensuring the success of autonomous missions. It reflects NASA's commitment to innovation and reliability in aerospace technology, providing a foundation for future developments in the field.
