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

TL;DR

This paper introduces Sandal, a modeling language that enables automatic, exhaustive fault-injection in message-passing distributed systems, facilitating verification of fault-tolerant behaviors without manual fault specification.

Contribution

The paper presents Sandal, a novel language with built-in support for abstracting and automatically injecting typical faults into models for verification purposes.

Findings

Automatic fault-injection enhances verification coverage.

Sandal effectively models fault-prone message-passing systems.

Verification of two-phase commit protocol under faults demonstrates practicality.

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.