Automated support for the design and validation of fault-tolerant parameterized systems : a case study
Articolo
Data di Pubblicazione:
2010
Citazione:
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: ELECTRONIC COMMUNICATIONS OF THE EASST. - ISSN 1863-2122. - 35(2010 Sep), pp. 1-14. ((Intervento presentato al 10. convegno International workshop on automated verification of critical systems (AVOCS) tenutosi a Düsseldorf nel 2010.
Abstract:
We propose a methodology to use the infinite state model checker MCMT, based on Satisfiability Modulo Theory techniques, for assisting in the design of fault tolerant algorithms. To prove the practical viability of our methodology, we apply it to formally check the agreement property of the reliable broadcast protocols of Chandra and Toueg.
Tipologia IRIS:
01 - Articolo su periodico
Keywords:
fault tolerant algorithms; infinite state model checking; parameter- ized verification; satisfiability modulo theories
Elenco autori:
F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G.P. Rossi
Link alla scheda completa: