Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study

Timed Failure Propagation Graphs (TFPGs) are used in the design of safety-critical systems as a way of modeling failure propagation, and to support the evaluation and implementation of functions for Fault Detection, Isolation, and Recovery (FDIR). TFPGs are a very rich formalism: they enable modeling Boolean combinations of faults and events, and quantitative delays between them. Several formal techniques have been recently developed to analyze them as stand-alone models or to compare them to models that describe the more detailed dynamics of the system of reference, specifically under faulty conditions. In this paper we present several case studies that apply TFPGs to Solar Orbiter, an ESA deep-space probe under development by Airbus. The mission is characterized by high requirements on on-board autonomy and FDIR. We focus on three possible application areas: hardware-to-software propagations, system-level propagations, and propagations across architectural hierarchies. The case studies show the added value of TFPGs for safety analysis and FDIR validation, as well as the scalability of available analysis tools for non-trivial industrial problems