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

Alexandre Albore, Silvano Dal Zilio, Marie De Roquemaurel, Christel Seguin, Pierre Virelizier
In ERTS 2018 — 9th European Congress on Embedded Real Time Software and Systems, jan 2018.

 PDF  HAL-01709008

Abstract

#

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.

Citation

#

@InProceedings{DalzilioS:ertss2018fdir,
   author    = {Albore, Alexandre and {Dal Zilio}, Silvano and {De Roquemaurel}, Marie and Seguin, Christel and Virelizier, Pierre},
   title     = {{Timed Formal Model and Verification of Satellite FDIR in Early Design Phase}},
   booktitle = {ERTS 2018 -- 9th European Congress on Embedded Real Time Software and Systems},
   month     = jan, 
   year      = 2018
}