Analyzing the propagation of faults is part of the preliminary safety assessment for complex safety-critical systems. A recent work proposes an SMT-based approach to deal with propagation of faults in presence of circular dependencies. The set of all the fault configurations that cause the violation of a property, also referred to as the set of minimal cut sets, is computed by means of repeated calls to the SMT solver, hence enumerating all minimal models of an SMT formula. Circularity is dealt with by imposing a strict temporal order, using the theory of difference logic. In this paper, we explore the use of Answer-Set Programming to tackle the same problem. We propose two encodings, leveraging the notion of stable model. The first approach deals with cycles in the encoding, while the second relies on ASP Modulo Acyclicity (ASPMA). We experimentally evaluate the three approaches on a comprehensive set of benchmarks. The first ASP-based encoding significantly outperforms the SMT-based approach; the ASPMA-based encoding, on the other hand, does not yield the expected performance gains.

Analysis of Cyclic Fault Propagation via ASP

Marco Bozzano;Alessandro Cimatti;Alberto Griggio;Martin Jonas;
2022-01-01

Abstract

Analyzing the propagation of faults is part of the preliminary safety assessment for complex safety-critical systems. A recent work proposes an SMT-based approach to deal with propagation of faults in presence of circular dependencies. The set of all the fault configurations that cause the violation of a property, also referred to as the set of minimal cut sets, is computed by means of repeated calls to the SMT solver, hence enumerating all minimal models of an SMT formula. Circularity is dealt with by imposing a strict temporal order, using the theory of difference logic. In this paper, we explore the use of Answer-Set Programming to tackle the same problem. We propose two encodings, leveraging the notion of stable model. The first approach deals with cycles in the encoding, while the second relies on ASP Modulo Acyclicity (ASPMA). We experimentally evaluate the three approaches on a comprehensive set of benchmarks. The first ASP-based encoding significantly outperforms the SMT-based approach; the ASPMA-based encoding, on the other hand, does not yield the expected performance gains.
978-3-031-15706-6
File in questo prodotto:
File Dimensione Formato  
main.pdf

solo utenti autorizzati

Descrizione: Preprint
Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 671.41 kB
Formato Adobe PDF
671.41 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11582/335527
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact