Timed Formal Model and Verification of Satellite FDIR in Early Design Phase

International audienceRegular Paper Abstract 1 In a previous work, we proposed an extension of the AltaRica language and tools to deal with the modelling and analysis of failures propagation in presence of timed and temporal constraints. This need is crucial in the space industry, where safety functionalities raise new challenges for the early validation of systems during model conception. This paper focuses on the application of our approach to the Failure Detection Isolation and Recovery (FDIR) mechanisms of the Attitude and Orbit Control System (AOCS) of a satellite. We discuss the modelling methodology applied to this system and its properties, as well as the tractability of the model-checking analysis. 1 An Expression of Industrial Needs and Requirements Failure Detection, Isolation and Recovery (FDIR) functions are implemented aboard satellites in order to detect the occurrence of failures and to prevent the failure from propagating in the whole system, which could cause critical events and thus jeopardize the mission. The complexity of the FDIR verification and validation (V&V) increases with the system complexity. As systems include more and more interacting functions and functional modes, it becomes harder to evaluate at the overall system level the effects of local failures. That is even truer when we consider the effects of time. Indeed, unexpected behavior can arise from a bad timing of events. Timing constraints allow to represent the impact of computation times, delays on the propagation of failures, and the reaction time of the reconfigurations steps triggered in reaction to failure detection. Thus, new models and tools are needed to assist early V&V of the on-board processes and FDIR design. Thomas and Blanquart [1] describe a process to model FDIR satellite functions. This process requires to model failure propagation, detection, and recovery times, which requires modelling languages expressive enough to support complex system modelling. Associated tools should provide automatic verification that on-board FDIR functions are correct despite latency in failure 1 We thank Jean-Paul Blanquart of AIRBUS Defence and Space for his kindness in discussing the FDIR model, and the evaluation of requirements for AOCS mode during the assessment of the scalability of the approach