CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Semi-Formal Development of a Fault-Tolerant Leader Election Protocol in Erlang

Koen Claessen (Institutionen för datavetenskap, Formella metoder ; Institutionen för datavetenskap, Funktionell programmering) ; Hans Svensson (Institutionen för datavetenskap, Formella metoder) ; Thomas Arts
Lecture Notes in Computer Science (0302-9743). Vol. 3395 (2005), p. 140-154.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: testing, model checking, abstraction



Denna post skapades 2006-10-09. Senast ändrad 2014-05-23.
CPL Pubid: 2544

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)
Institutionen för datavetenskap, Funktionell programmering (2002-2004)

Ämnesområden

Information Technology

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving