{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:35:14Z","timestamp":1761489314000,"version":"3.41.0"},"reference-count":6,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,11]],"date-time":"2014-02-11T00:00:00Z","timestamp":1392076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2014,2,11]]},"abstract":"<jats:p>The 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.<\/jats:p>","DOI":"10.1145\/2557833.2560583","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T14:08:32Z","timestamp":1392732512000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal validation of fault management design solutions"],"prefix":"10.1145","volume":"39","author":[{"given":"Corrina","family":"Gibson","sequence":"first","affiliation":[{"name":"Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA"}]},{"given":"Robert","family":"Karban","sequence":"additional","affiliation":[{"name":"European Southern Observatory, Garching, Germany"}]},{"given":"Luigi","family":"Andolfato","sequence":"additional","affiliation":[{"name":"European Southern Observatory, Garching, Germany"}]},{"given":"John","family":"Day","sequence":"additional","affiliation":[{"name":"Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA"}]}],"member":"320","published-online":{"date-parts":[[2014,2,11]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Meakin P. 2013. SMAP Project System Fault Protection FDD initial release Jet Propulsion Laboratory D-61607.  Meakin P. 2013. SMAP Project System Fault Protection FDD initial release Jet Propulsion Laboratory D-61607."},{"key":"e_1_2_1_2_1","unstructured":"Meakin P. 2013. SMAP Project System Modes and Configuration FDD Rev A Jet Propulsion Laboratory D-61605.  Meakin P. 2013. SMAP Project System Modes and Configuration FDD Rev A Jet Propulsion Laboratory D-61605."},{"key":"e_1_2_1_3_1","volume-title":"ICALEPCS","author":"Andolfato L.","year":"2011","unstructured":"Andolfato , L. , Chiozzi , G. Migliorini , N. , Morales , C. , ICALEPCS 2011 . A Platform Independent Framework for Statecharts Code Generation Andolfato, L., Chiozzi, G. Migliorini, N., Morales, C., ICALEPCS 2011. A Platform Independent Framework for Statecharts Code Generation"},{"key":"e_1_2_1_4_1","volume-title":"et al","author":"Amedro B.","year":"2008","unstructured":"Amedro , B. et al . 2008 . Current State of Java for HPC, INRIA Rapport Technique Nr . 0353 Amedro, B. et al. 2008. Current State of Java for HPC, INRIA Rapport Technique Nr. 0353"},{"key":"e_1_2_1_5_1","unstructured":"W3C. 2013. Statechart XML (SCXML): State Machine Notation for Control Abstraction (www.w3.org\/TR\/scxml\/)  W3C. 2013. Statechart XML (SCXML): State Machine Notation for Control Abstraction (www.w3.org\/TR\/scxml\/)"},{"volume-title":"Jet Propulsion Laboratory","author":"Soil Moisture Active Passive","key":"e_1_2_1_6_1","unstructured":"Soil Moisture Active Passive . Jet Propulsion Laboratory , California Institute of Technology . http:\/\/www.jpl.nasa.gov\/missions\/details.php?id=5995 Soil Moisture Active Passive. Jet Propulsion Laboratory, California Institute of Technology. http:\/\/www.jpl.nasa.gov\/missions\/details.php?id=5995"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560583","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2557833.2560583","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:59Z","timestamp":1750232099000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560583"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,11]]},"references-count":6,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2,11]]}},"alternative-id":["10.1145\/2557833.2560583"],"URL":"https:\/\/doi.org\/10.1145\/2557833.2560583","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2014,2,11]]},"assertion":[{"value":"2014-02-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}