Computer Science laboratory, Ericsson Utvecklings AB (SWEDEN)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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 our FTP 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 our FTP 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 our FTP site in PDF or PostScript
Dr. Thomas Arts
Department of Applied Information Technology
IT University of Göteborg
P.O. Box 8718
402 75 Göteborg
Tel: +46 (0)31 772 60 31
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|