Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study
Contributo in Atti di convegno
Data di Pubblicazione:
2010
Citazione:
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 [10.1007/978-3-642-15763-9_36].
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.
Tipologia IRIS:
03 - Contributo in volume
Keywords:
infinite state model-checking ; fault tolerant systems ; satisfiability modulo theories
Elenco autori:
F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G.P. Rossi
Link alla scheda completa:
Titolo del libro:
Distributed computing : 24th international symposium, DSC 2010, Cambridge,MA, USA, september 13-15, 2010 : proceedings