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 and Jan KŘETÍNSKÝ

Basic information

Original name

Model Checking for Proving and Improving Fault Tolerance of Satellites

Authors

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

Edition

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

Publisher

IEEE

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

printed version "print"

Organization unit

Faculty of Informatics

ISSN

DOI

http://dx.doi.org/10.1109/AERO55745.2023.10115801

UT WoS

001008282003040

Abstract

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 and 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 pp. ISSN 1095-323X. Available from: https://dx.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 = {http://dx.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  - JOUR
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 and 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 pp. ISSN~1095-323X. Available from: https://dx.doi.org/10.1109/AERO55745.2023.10115801.

Detailed Information on Publication Record