Další formáty:
BibTeX
LaTeX
RIS
@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 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://dx.doi.org/10.1109/AERO55745.2023.10115801.
|