Tech Briefs

A number of advantages of modeling fault protection logical design, executing the model, and running a model checker are identified.

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:

  1. Designing logical behavior of a system in a model is less prone to human error.
  2. Simulating multi-fault, multi-response fault injection tests in the model increases the test domain and verifies system behavior.
  3. Auto-generation of event reports for fault injection tests provides a useful product for understanding system behavior (designing and testing).
  4. Validating the logical design of the system against domain-specific constraints.
  5. 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 email address is being protected from spambots. You need JavaScript enabled to view it.. Refer to NPO-49337.

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.

Please Login at the top of the page to download.

The U.S. Government does not endorse any commercial product, process, or activity identified on this web site.