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 [10.1007/978-3-642-15763-9_36].
Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study
S. GhilardiSecondo
;E. Pagani;G.P. RossiUltimo
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.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
