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.

Efficient SMT-Based Analysis of Failure Propagation / Bozzano, Marco; Cimatti, Alessandro; Fernandes Pires, Anthony; Griggio, Alberto; Jonas, Martin; Kimberly, Greg. - 12760:(2021), pp. 209-230. (Intervento presentato al convegno Computer Aided Verification - 33rd International Conference tenutosi a virtual nel 20-23 July 2021) [10.1007/978-3-030-81688-9_10].

Efficient SMT-Based Analysis of Failure Propagation

Alessandro Cimatti;Alberto Griggio;
2021-01-01

Abstract

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.
2021
Proceedings of Computer Aided Verification - 33rd International Conference, (CAV2021), Virtual Event, Part II
Cham, Switzerland
Springer
Bozzano, Marco; Cimatti, Alessandro; Fernandes Pires, Anthony; Griggio, Alberto; Jonas, Martin; Kimberly, Greg
Efficient SMT-Based Analysis of Failure Propagation / Bozzano, Marco; Cimatti, Alessandro; Fernandes Pires, Anthony; Griggio, Alberto; Jonas, Martin; Kimberly, Greg. - 12760:(2021), pp. 209-230. (Intervento presentato al convegno Computer Aided Verification - 33rd International Conference tenutosi a virtual nel 20-23 July 2021) [10.1007/978-3-030-81688-9_10].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/342953
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact