Development of a Verified Erlang Program for Resource Locking.

Organisation:	Computer Science laboratory, Ericsson Utvecklings AB (SWEDEN)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Distributed Algorithms.
Period:	2000-2001
Size:	n/a
Description:	This case-study concerns the development of a distributed locker algorithm (a variant of the algorithm used in Ericsson's AXD 301 ATM switch) by using formal methods. The system under study consists of several processes that execute concurrently and access one or more resources. A locker process is responsible for handling the requests for access to resources in such a way that all client processes eventually get their demanded access, but no two clients get access to the same resource at the same time. A state of the locker contains, for each resource, an access field denoting the client that has currently access to the resource, and a pending list of the clients that want to access the resource. The locker maintains a combined representation of the pending lists associated to all resources and must decide which client will get access to a resource. The locker system was implemented in Erlang, the locker and the clients being represented as Erlang processes following a client-server scheme. The Erlang specification was then automatically translated in muCRL. The translation consists of two steps: (1) an Erlang to Erlang transformation, which produces an Erlang code equivalent to the initial one, but optimized for verification; (2) a translation of the collection of Erlang modules into one muCRL specification. The muCRL toolset was then used for constructing the Labeled Transition Systems (LTS) corresponding to the resulting muCRL specifications. Several configurations were considered, up to three clients and four resources, the largest one having an LTS model with about one million states. There are three desired properties for the distributed locker system: deadlock freedom, mutual exclusion, and absence of starvation. The first two properties have been expressed as regular alternation-free mu-calculus formulas and verified on the LTS models using the EVALUATOR 3.0 model-checker of CADP. For absence of starvation only a weaker variant of the property was checked (fair reachability of accesses to resources), because it seems difficult to give a full characterization of this property using regular alternation-free mu-calculus.
Conclusions:	The main contribution of this work lays in the development of an automatic translation of a class of Erlang programs to muCRL. This allows to benefit from "push-button" verification features during the development of Erlang programs, by using the muCRL toolset for constructing the LTS models corresponding to Erlang programs, and the CADP toolset for automatically verifying correctness properties expressed in temporal logic. The approach proposed was illustrated on a case-study concerning the development of a distributed locker system used in a product of Ericsson.
Publications:	[Arts-Benac-01] Thomas Arts and Clara Benac Earle. "Development of a Verified Erlang Program for Resource Locking". Proceedings of the 6th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2001 (Paris, France), pp. 131-145, June 2001. Available on-line at: http://www.erlang.se/publications/clara2.ps or from the CADP Web site in PDF or PostScript [Arts-Benac-Derrick-02] Thomas Arts, Clara Benac Earle, and John Derrick. "Verifying Erlang Code: A Resource Locker Case-Study". In Lars-Henrik Eriksson and Peter A. Lindsay, editors, Proceedings of the 11th International Symposium of Formal Methods Europe FME'2002 (Copenhagen, Denmark), Lecture Notes in Computer Science vol. 2391, pp. 184-203. Springer Verlag, July 2002. Available from the CADP Web site in PDF or PostScript [Arts-Benac-Derrick-04] Thomas Arts, Clara Benac Earle, and John Derrick. "Development of a Verified Erlang Program for Resource Locking". International Journal on Software Tools for Technology Transfer (STTT), Volume 5(2-3), pp. 205-220, March 2004. Preliminary version available on-line at: http://www.cs.kent.ac.uk/pubs/2003/1712/content.pdf or from the CADP Web site in PDF or PostScript
Contact:	Dr. Thomas Arts Program Manager Department of Applied Information Technology IT University of Göteborg P.O. Box 8718 402 75 Göteborg Sweden Tel: +46 (0)31 772 60 31 E-mail: [email protected]
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