Model Checking for Proving and Improving Fault Tolerance of
Satellites

D 2023

Model Checking for Proving and Improving Fault Tolerance of Satellites

KIESBYE, Jonis; Kush GROVER a Jan KŘETÍNSKÝ

Základní údaje

Originální název

Model Checking for Proving and Improving Fault Tolerance of Satellites

Autoři

KIESBYE, Jonis; Kush GROVER a Jan KŘETÍNSKÝ

Vydání

NEW YORK, 2023 IEEE AEROSPACE CONFERENCE, 9 s. 2023

Nakladatel

IEEE

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISSN

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 8. 4. 2024 06:13, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Developing the Fault Detection, Isolation & Recovery (FDIR) policy often happens late in the design phase of a spacecraft and might reveal significant gaps in the redundancy concept. We propose a process for continuously analyzing and improving the architecture of a spacecraft throughout the design phase to ensure successful fault isolation and recovery. The systems engineer provides a graph of the system's architecture containing the functional modes, the hardware components, and their dependency on each other as an input and gets back a weakness report listing the gaps in the redundancy concept. Overlaying the sub-graphs for every fault scenario allows us to reason about the feasibility of fault isolation and recovery. The graph is automatically converted to a Markov Decision Process for use with a model checker to generate a control policy for the FDIR process. The model is optimized by pruning inefficient branches with Monte Carlo Tree Search. We export this policy as a decision tree that ensures explainability, fast execution, and low memory requirements during runtime. We also generate C-code for fault isolation and reconfiguration that can be integrated in the FDIR software. The tool was used on system architectures created in the Modular ADCS project which is part of ESA's GSTP program. In this context, it helped to yield an effective redundancy concept with minimum overhead and dramatically reduce the programming effort for FDIR routines. Since we use model checking for the analysis, the designer gains formal verification of the robustness towards faults.

Citovat

KIESBYE, Jonis; Kush GROVER a Jan KŘETÍNSKÝ. Model Checking for Proving and Improving Fault Tolerance of Satellites. In 978-1-6654-9032-0. 2023 IEEE AEROSPACE CONFERENCE. NEW YORK: IEEE, 2023, 9 s. ISSN 1095-323X. Dostupné z: https://doi.org/10.1109/AERO55745.2023.10115801.

@inproceedings{2392229,
   author = {Kiesbye, Jonis and Grover, Kush and Křetínský, Jan},
   address = {NEW YORK},
   booktitle = {2023 IEEE AEROSPACE CONFERENCE},
   doi = {https://doi.org/10.1109/AERO55745.2023.10115801},
   editor = {978-1-6654-9032-0},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {NEW YORK},
   publisher = {IEEE},
   title = {Model Checking for Proving and Improving Fault Tolerance of Satellites},
   year = {2023}
}

TY  - CONF
ID  - 2392229
AU  - Kiesbye, Jonis - Grover, Kush - Křetínský, Jan
PY  - 2023
TI  - Model Checking for Proving and Improving Fault Tolerance of Satellites
PB  - IEEE
CY  - NEW YORK
N2  - Developing the Fault Detection, Isolation & Recovery (FDIR) policy often happens late in the design phase of a spacecraft and might reveal significant gaps in the redundancy concept. We propose a process for continuously analyzing and improving the architecture of a spacecraft throughout the design phase to ensure successful fault isolation and recovery. The systems engineer provides a graph of the system's architecture containing the functional modes, the hardware components, and their dependency on each other as an input and gets back a weakness report listing the gaps in the redundancy concept. Overlaying the sub-graphs for every fault scenario allows us to reason about the feasibility of fault isolation and recovery. The graph is automatically converted to a Markov Decision Process for use with a model checker to generate a control policy for the FDIR process. The model is optimized by pruning inefficient branches with Monte Carlo Tree Search. We export this policy as a decision tree that ensures explainability, fast execution, and low memory requirements during runtime. We also generate C-code for fault isolation and reconfiguration that can be integrated in the FDIR software. The tool was used on system architectures created in the Modular ADCS project which is part of ESA's GSTP program. In this context, it helped to yield an effective redundancy concept with minimum overhead and dramatically reduce the programming effort for FDIR routines. Since we use model checking for the analysis, the designer gains formal verification of the robustness towards faults.
ER  -

KIESBYE, Jonis; Kush GROVER a Jan KŘETÍNSKÝ. Model Checking for Proving and Improving Fault Tolerance of Satellites. In 978-1-6654-9032-0. \textit{2023 IEEE AEROSPACE CONFERENCE}. NEW YORK: IEEE, 2023, 9 s. ISSN~1095-323X. Dostupné z: https://doi.org/10.1109/AERO55745.2023.10115801.

Přehled o publikaci