Verifying Fault-Tolerant Erlang Programs

Organisation:	University Carlos III and Polytechnical University of Madrid (SPAIN) University of Sheffield (UNITED KINGDOM)
Method:	Erlang muCRL
Tools used:	etomcrl muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Embedded Systems.
Period:	2005
Size:	n/a
Description:	This case study addresses the verification of fault-tolerant generic servers written in the functional programming language Erlang and its associated component library OTP (Open Telephone Platform) for developing fault-tolerant telecom applications. The approach is based on an automatic translation of Erlang programs into muCRL. This translation takes care of implicit communications between clients and servers. For instance, whenever a client crashes, Erlang/OTP guarantees that the server receives an exit message. Since these additional messages are not specific to an application, but belong to the generic component, they can be inserted automatically in the generated muCRL code. In a second step, the LTS (labeled transition system) corresponding to the muCRL model is generated. This LTS is then used to verify with EVALUATOR several properties, such as deadlock freedom, mutual exclusion, or non-starvation. This approach is illustrated on a generic fail-safe locker service, which offers clients to acquire and release a lock; requests for the lock are buffered, if the lock is already granted to another client. For the verification of mutual exclusion, the use of EVALUATOR proved to be very helpful in debugging the implementation and the formulae. For instance, the mutual exclusion properties have to take into account that a client might crash after obtaining the lock, but before freeing the lock. Also, for a scenario with three clients, EVALUATOR found in a few seconds a counter example in an erroneous implementation of the procedure handling client crashes.
Conclusions:	Formal methods and model checking prove to be useful steps in the design process of fault-tolerant concurrent applications, by allowing an accurate description of failures and by facilitating debugging based on automatically generated counter examples.
Publications:	[Benac-Fredlund-05] Clara Benac Earle and Lars-Åke Fredlund. "Verification of Language Based Fault-Tolerance". In R. Moreno-Díaz, F. Pichler, and A. Quesada-Arencibia (Eds.), Proceedings of the 10th International Conference on Computer Aided Systems Theory EUROCAST 2005 (Las Palmas de Gran Canaria, Spain), LNCS vol. 3643, pp. 140-149, Springer Verlag, February 2005. Available on-line from the CADP Web site in PDF or PostScript [Benac-Fredlund-Derrick-05] Clara Benac Earle, Lars-Åke Fredlund, and John Derrick. "Verifying Fault-Tolerant Erlang Programs". In K. F. Sagonas and J. Armstrong (Eds.), Proceedings of the 2005 ACM SIGPLAN Workshop on Erlang (Tallinn, Estonia), pages 26-34, September 2005. Available on-line from the CADP Web site in PDF or PostScript
Contact:	Prof. John Derrick Department of Computer Science University of Sheffield Regent Court, 211 Portobello St., Sheffield S1 4DP United Kingdom Tel: +44 (0)114 22 21849 Fax: +44 (0)114 22 21810 E-mail: J.Derrick@dcs.shef.ac.uk
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page