Specification, Synthesis and Verification of Software-Based Control Protocols for Fault-Tolerant Space Systems
Technical point of contact: Dr. Scott Erwin and Dr. Fred Leve, Air Force Research Lab (RV)
Period of activity: 2015-2016
Overview of the Project
The objective of this proposal is to develop (i) formal specifications of correctness for software-based control protocols for space systems and (ii) model-based verification and correct-by-construction synthesis methods and tools against these specifications. We initially focus on the correctness of mode switching sequences and logics, reconfiguration strategies to recover from failures, automated debugging of such strategies, and systematic identification of the causes for failures.
The proposed techniques will be demonstrated on a case study (i.e., models and specifications) that represents the typical complexity of attitude and orbit control systems. A case study of interest contains a number of modes for normal as well as faulty, backup, fail-safe, recovery operations. Each mode contains dynamics at fidelity levels representative of the typical dynamics in the attitude and orbit control of spacecraft. The modes (and the dynamics in each mode) and the allowed mode transitions may generate scenarios that lead to anomalous mode switching sequences.