MOD*2014 Talk

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

Masaya Suzuki & Takuo Watanabe
1st Workshop on Logics and Model-Checking for Self-* Systems (MOD* 2014),
Centro Residenziale Universitario di Bertinoro, Bertinoro, Italy, 2014/9/12.

Abstract

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.

Publication

Masaya Suzuki & Takuo Watanabe, A Language Support for Exhaustive Fault-Injection in Message-Passing System Models, In Proceedings First Workshop on Logics and Model-checking for Self-* Systems, Electronic Proceedings in Theoretical Computer Science, Vol. 168, pp. 45-58, DOI:10.4204/EPTCS.168.4, Nov., 2014.