Informace o publikaci
Efficient SMT-Based Analysis of Failure Propagation
| Autoři | |
|---|---|
| Rok publikování | 2021 |
| Druh | Článek ve sborníku |
| Konference | Computer Aided Verification. CAV 2021. |
| Citace | |
| www | https://link.springer.com/chapter/10.1007/978-3-030-81688-9_10 |
| Doi | http://dx.doi.org/10.1007/978-3-030-81688-9_10 |
| Popis | 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. |