Informace o publikaci

Efficient SMT-Based Analysis of Failure Propagation

Autoři

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

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.

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info