Efficient SMT-Based Analysis of Failure Propagation

D 2021

Efficient SMT-Based Analysis of Failure Propagation

BOZZANO, Marco; Alessandro CIMATTI; Anthony FERNANDES PIRES; Alberto GRIGGIO; Martin JONÁŠ et al.

Základní údaje

Originální název

Efficient SMT-Based Analysis of Failure Propagation

Autoři

BOZZANO, Marco; Alessandro CIMATTI; Anthony FERNANDES PIRES; Alberto GRIGGIO; Martin JONÁŠ a Greg KIMBERLY

Vydání

Cham, Computer Aided Verification. CAV 2021. od s. 209-230, 22 s. 2021

Nakladatel

Springer

Další údaje

Typ výsledku

Stať ve sborníku

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Označené pro přenos do RIV

ISBN

978-3-030-81687-2

DOI

https://doi.org/10.1007/978-3-030-81688-9_10

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 6. 11. 2023 20:44, RNDr. Martin Jonáš, Ph.D.

Anotace

V originále

The process of developing civil aircraft and their related systems includes multiple phases of Preliminary Safety Assessment (PSA). An objective of PSA is to link the classification of failure conditions and effects (produced in the functional hazard analysis phases) to appropriate safety requirements for elements in the aircraft architecture. A complete and correct preliminary safety assessment phase avoids potentially costly revisions to the design late in the design process. Hence, automated ways to support PSA are an important challenge in modern aircraft design. A modern approach to conducting PSAs is via the use of abstract propagation models, that are basically hyper-graphs where arcs model the dependency among components, e.g. how the degradation of one component may lead to the degraded or failed operation of another. Such models are used for computing failure propagations: the fault of a component may have multiple ramifications within the system, causing the malfunction of several interconnected components. A central aspect of this problem is that of identifying the minimal fault combinations, also referred to as minimal cut sets, that cause overall failures. In this paper we propose an expressive framework to model failure propagation, catering for multiple levels of degradation as well as cyclic and nondeterministic dependencies. We define a formal sequential semantics, and present an efficient SMT-based method for the analysis of failure propagation, able to enumerate cut sets that are minimal with respect to the order between levels of degradation. In contrast with the state of the art, the proposed approach is provably more expressive, and dramatically outperforms other systems when a comparison is possible.

Citovat

BOZZANO, Marco; Alessandro CIMATTI; Anthony FERNANDES PIRES; Alberto GRIGGIO; Martin JONÁŠ a Greg KIMBERLY. Efficient SMT-Based Analysis of Failure Propagation. In Silva, A., Leino, K.R.M. Computer Aided Verification. CAV 2021. Cham: Springer, 2021, s. 209-230. ISBN 978-3-030-81687-2. Dostupné z: https://doi.org/10.1007/978-3-030-81688-9_10.

@inproceedings{2335577,
   author = {Bozzano, Marco and Cimatti, Alessandro and Fernandes Pires, Anthony and Griggio, Alberto and Jonáš, Martin and Kimberly, Greg},
   address = {Cham},
   booktitle = {Computer Aided Verification. CAV 2021.},
   doi = {https://doi.org/10.1007/978-3-030-81688-9_10},
   editor = {Silva, A., Leino, K.R.M.},
   howpublished = {tištěná verze "print"},
   location = {Cham},
   isbn = {978-3-030-81687-2},
   pages = {209-230},
   publisher = {Springer},
   title = {Efficient SMT-Based Analysis of Failure Propagation},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-81688-9_10},
   year = {2021}
}

TY  - CONF
ID  - 2335577
AU  - Bozzano, Marco - Cimatti, Alessandro - Fernandes Pires, Anthony - Griggio, Alberto - Jonáš, Martin - Kimberly, Greg
PY  - 2021
TI  - Efficient SMT-Based Analysis of Failure Propagation
PB  - Springer
CY  - Cham
SN  - 9783030816872
UR  - https://link.springer.com/chapter/10.1007/978-3-030-81688-9_10
N2  - The process of developing civil aircraft and their related systems includes multiple phases of Preliminary Safety Assessment (PSA). An objective of PSA is to link the classification of failure conditions and effects (produced in the functional hazard analysis phases) to appropriate safety requirements for elements in the aircraft architecture. A complete and correct preliminary safety assessment phase avoids potentially costly revisions to the design late in the design process. Hence, automated ways to support PSA are an important challenge in modern aircraft design. A modern approach to conducting PSAs is via the use of abstract propagation models, that are basically hyper-graphs where arcs model the dependency among components, e.g. how the degradation of one component may lead to the degraded or failed operation of another. Such models are used for computing failure propagations: the fault of a component may have multiple ramifications within the system, causing the malfunction of several interconnected components. A central aspect of this problem is that of identifying the minimal fault combinations, also referred to as minimal cut sets, that cause overall failures. In this paper we propose an expressive framework to model failure propagation, catering for multiple levels of degradation as well as cyclic and nondeterministic dependencies. We define a formal sequential semantics, and present an efficient SMT-based method for the analysis of failure propagation, able to enumerate cut sets that are minimal with respect to the order between levels of degradation. In contrast with the state of the art, the proposed approach is provably more expressive, and dramatically outperforms other systems when a comparison is possible.
ER  -

BOZZANO, Marco; Alessandro CIMATTI; Anthony FERNANDES PIRES; Alberto GRIGGIO; Martin JONÁŠ a Greg KIMBERLY. Efficient SMT-Based Analysis of Failure Propagation. In Silva, A., Leino, K.R.M. \textit{Computer Aided Verification. CAV 2021.}. Cham: Springer, 2021, s.~209-230. ISBN~978-3-030-81687-2. Dostupné z: https://doi.org/10.1007/978-3-030-81688-9\_{}10.

Přehled o publikaci