A Language Support for Exhaustive Fault-Injection in Message-Passing System Models

Masaya Suzuki
(Department of Computer Science, Tokyo Institute of Technology)
Takuo Watanabe
(Department of Computer Science, Tokyo Institute of Technology)

This paper presents an approach towards specifying and verifying adaptive distributed systems. We here take fault-handling as an example of adaptive behavior and propose a modeling language Sandal for describing fault-prone message-passing systems. One of the unique mechanisms of the language is a linguistic support for abstracting typical faults such as unexpected termination of processes and random loss of messages. The Sandal compiler translates a model into a set of NuSMV modules. During the compilation process, faults specified in the model will be woven into the output. One can thus enjoy full-automatic exhaustive fault-injection without writing faulty behaviors explicitly. We demonstrate the advantage of the language by verifying a model of the two-phase commit protocol under faulty environment.

In Marcello Maria Bersani, Davide Bresolin, Luca Ferrucci and Manuel Mazzara: Proceedings First Workshop on Logics and Model-checking for Self-* Systems (MOD* 2014), Bertinoro, Italy, 12th September 2014, Electronic Proceedings in Theoretical Computer Science 168, pp. 45–58.
Published: 13th November 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.168.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org