NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal Validation of Fault Management Design SolutionsThe work presented in this paper describes an approach used to develop SysML modeling patterns to express the behavior of fault protection, test the model's logic by performing fault injection simulations, and verify the fault protection system's logical design via model checking. A representative example, using a subset of the fault protection design for the Soil Moisture Active-Passive (SMAP) system, was modeled with SysML State Machines and JavaScript as Action Language. The SysML model captures interactions between relevant system components and system behavior abstractions (mode managers, error monitors, fault protection engine, and devices/switches). Development of a method to implement verifiable and lightweight executable fault protection models enables future missions to have access to larger fault test domains and verifiable design patterns. A tool-chain to transform the SysML model to jpf-Statechart compliant Java code and then verify the generated code via model checking was established. Conclusions and lessons learned from this work are also described, as well as potential avenues for further research and development.
Document ID
20150007990
Acquisition Source
Jet Propulsion Laboratory
Document Type
Conference Paper
External Source(s)
Authors
Gibson, Corrina
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Karban, Robert
(European Southern Observatory Garching, Germany)
Andolfato, Luigi
(European Southern Observatory Garching, Germany)
Day, John
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
May 12, 2015
Publication Date
November 12, 2013
Subject Category
Computer Programming And Software
Meeting Information
Meeting: Java Pathfinder Workshop 2013
Location: Palo Alto, CA
Country: United States
Start Date: November 12, 2013
Sponsors: NASA Headquarters
Distribution Limits
Public
Copyright
Other
Keywords
Statechart
Model Checking
Fault Protection
SysML

Available Downloads

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