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

Autor: Alexandre Albore, Silvano Dal Zilio, Marie de Roquemaurel, Christel Seguin, Pierre Virelizier
Přispěvatelé: IRT Saint Exupéry - Institut de Recherche Technologique, Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, ONERA - The French Aerospace Lab [Toulouse], ONERA, Airbus Defence and Space [Toulouse], Safran Tech, Équipe Verification de Systèmes Temporisés Critiques ( LAAS-VERTICS ), Laboratoire d'analyse et d'architecture des systèmes [Toulouse] ( LAAS ), Institut National Polytechnique [Toulouse] ( INP ) -Institut National des Sciences Appliquées - Toulouse ( INSA Toulouse ), Institut National des Sciences Appliquées ( INSA ) -Institut National des Sciences Appliquées ( INSA ) -Université Paul Sabatier - Toulouse 3 ( UPS ) -Centre National de la Recherche Scientifique ( CNRS ) -Institut National Polytechnique [Toulouse] ( INP ) -Institut National des Sciences Appliquées - Toulouse ( INSA Toulouse ), Institut National des Sciences Appliquées ( INSA ) -Institut National des Sciences Appliquées ( INSA ) -Université Paul Sabatier - Toulouse 3 ( UPS ) -Centre National de la Recherche Scientifique ( CNRS ), ONERA - The French Aerospace Lab ( Toulouse ), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)
Jazyk: angličtina
Rok vydání: 2018
Předmět:
Zdroj: 9th European Congress on Embedded Real Time Software and Systems (ERTS 2018)
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France. 10p
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France. 10p., 2018, 〈http://www.erts2018.org/〉
HAL
Popis: International audience; Regular 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.
Databáze: OpenAIRE
Externí odkaz: