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.
Automated support for the design and validation of fault tolerant Parameterized systems: A case study / Alberti, F.; Ghilardi, S.; Pagani, E.; Ranise, S.; Rossi, G. P.. - In: ELECTRONIC COMMUNICATIONS OF THE EASST. - ISSN 1863-2122. - 35:(2010). (Intervento presentato al convegno Automated Verification of Critical Systems 2010 tenutosi a Germany nel 20-23/09/2010) [10.14279/tuj.eceasst.35.543.581].
Automated support for the design and validation of fault tolerant Parameterized systems: A case study
Ranise S.;
2010-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
