A basic concept in modeling fault tolerant systems is that anticipated faults, being obviously outside of our control, may or may not occur. A fault tolerant system design can be proved to correctly behave under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behavior can be applied to verify the correctness of the design. Another activity that must be considered in fault tolerance is the issue of fault detection, since the existence of undetectable faults makes the system more vulnerable. The usage of model checking and temporal logic gives opportunities to better analyze the system behavior in presence of faults and to identify undetectable faults.

Application of Model Checking to Fault Tolerance Analysis

Bernardeschi C.
;
Domenici A.
2019-01-01

Abstract

A basic concept in modeling fault tolerant systems is that anticipated faults, being obviously outside of our control, may or may not occur. A fault tolerant system design can be proved to correctly behave under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behavior can be applied to verify the correctness of the design. Another activity that must be considered in fault tolerance is the issue of fault detection, since the existence of undetectable faults makes the system more vulnerable. The usage of model checking and temporal logic gives opportunities to better analyze the system behavior in presence of faults and to identify undetectable faults.
2019
Bernardeschi, C.; Domenici, A.
File in questo prodotto:
File Dimensione Formato  
ABP.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 311.58 kB
Formato Adobe PDF
311.58 kB Adobe PDF Visualizza/Apri

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/11568/1016595
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact