Algorithms for ensuring fault tolerance are key ingredients in many applications such as avionics and networking. There is an increasing demand to integrate (formal) validation in the design process of these algorithms as they are often part of safety critical systems. We propose the use of an infinite state model checker for safety properties, called mcmt, to assist in the design of the considered class of algorithms. We apply mcmt to the verification of the Agreement property of a reliable broadcast algorithm proposed by Chandra and Toueg. Agreement as the safety property to check.

Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study

Ranise, Silvio;
2010-01-01

Abstract

Algorithms for ensuring fault tolerance are key ingredients in many applications such as avionics and networking. There is an increasing demand to integrate (formal) validation in the design process of these algorithms as they are often part of safety critical systems. We propose the use of an infinite state model checker for safety properties, called mcmt, to assist in the design of the considered class of algorithms. We apply mcmt to the verification of the Agreement property of a reliable broadcast algorithm proposed by Chandra and Toueg. Agreement as the safety property to check.
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/11582/21329
 Attenzione

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

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