WCTP2014 Talk

Sandal: A Modeling Language Supporting Exhaustive Fault-Injection

Masaya Suzuki & Takuo Watanabe
4th Workshop on Computation: Theory and Practice (WCTP 2014), Manila, Oct. 6-7, 2014.

Abstract

Sandal is a modeling language designed for specifying and model-checking fault-prone message-passing systems. The language supports the modular description of typical faults including unexpected termination of processes, random loss of messages and timeout. Thus on defining a model in Sandal, one does not need to write such faulty actions explicitly intermingled with the primary behaviors of the model. The compiler of the language automatically weaves them and produces a set of NuSMV modules. This paper describes how the weaving mechanism works and demonstrates the usefulness of the language using an example.

Publication

Masaya Suzuki & Takuo Watanabe, Sandal: A Modeling Language Supporting Exhaustive Fault-Injection, In Theory and Practice of Computation, Proceedings of Workshop on Computation: Theory and Practice (WCTP2014), Jan., 2016.
World Scientific, pp. 1-12, DOI:10.1142/9789814730464_0001