We propose a methodology to use the infinite state model checker mcmt, based on the Satisfiability Modulo Theory technology, to assist in the design of fault tolerant algorithms. To prove the practical viability of our methodology, we applied it to formally check the agreement property of the reliable broadcast protocols of Chandra and Toueg.

Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study / F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G.P. Rossi - In: Distributed computing : 24th international symposium, DSC 2010, Cambridge,MA, USA, september 13-15, 2010 : proceedings / [a cura di] N. A. Lynch, A. A. Shvartsman. - Berlin : Springer, 2010. - ISBN 9783642157622. - pp. 392-394 (( Intervento presentato al 24. convegno International Symposium on Distributed Computing tenutosi a Cambridge, USA nel 2010.

Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study

S. Ghilardi;E. Pagani;G.P. Rossi
2010

Abstract

We propose a methodology to use the infinite state model checker mcmt, based on the Satisfiability Modulo Theory technology, to assist in the design of fault tolerant algorithms. To prove the practical viability of our methodology, we applied it to formally check the agreement property of the reliable broadcast protocols of Chandra and Toueg.
infinite state model-checking ; fault tolerant systems ; satisfiability modulo theories
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

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: http://hdl.handle.net/2434/153060
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 4
social impact