zbMATH — the first resource for mathematics

Semi-formal development of a fault-tolerant leader election protocol in Erlang. (English) Zbl 1081.68565
Grabowski, Jens (ed.) et al., Formal approaches to software testing. 4th international workshop, FATES 2004, Linz, Austria, September 21, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-25109-X/pbk). Lecture Notes in Computer Science 3395, 140-154 (2005).
Summary: We present a semi-formal analysis method for fault-tolerant distributed algorithms written in the distributed functional programming language Erlang. In this setting, standard model checking techniques are often too expensive or too limiting, whereas testing techniques often do not cover enough of the state space.
Our idea is to first run instances of the algorithm on generated stimuli, thereby creating traces of events and states. Then, using an abstraction function specified by the user, our tool generates from these traces an abstract state transition diagram of the system, which can be nicely visualized and thus greatly helps in debugging the system. Lastly, formal requirements of the system specified in temporal logic can be checked automatically to hold for the generated abstract state transition diagram. Because the state transition diagram is abstract, we know that the checked requirements hold for a lot more traces than just the traces we actually ran.
We have applied our method to a commonly used open-source fault-tolerant leader election algorithm, and discovered two serious bugs. We have also implemented a new algorithm that does not have these bugs.
For the entire collection see [Zbl 1069.68008].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages
68N18 Functional programming and lambda calculus
68W15 Distributed algorithms
Erlang; JPAX
Full Text: DOI