Abstract
In this paper we describe an industrial case-study on the development of formally verified code for Ericsson’s AXD 301 switch. For the formal verification of Erlang software we have developed a tool to apply model checking to communicating Erlang processes. We make effective use of Erlang’s design principles for large software systems to obtain relatively small models of specific Erlang programs. By assuming a correct implementation of the software components and embedding their semantics into our model, we can concentrate on the specific functionality of the components. We constructed a tool to automatically translate the Erlang code to a process algebra with data. Existing tools were used to generate the full state space and to formally verify properties stated in the modal μ-calculus.
As long as the specific functionality of the component has a finite state vector, we can generate a finite state space, even if the state space of the real Erlang system is infinite. In this paper we illustrate this by presenting a case-study based on a piece of software in Ericsson’s AXD 301 switch, which implements a distributed resource locker algorithm. Some of the key properties we proved are mutual exclusion and non-starvation for the program.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.L. Armstrong, S.R. Virding, M.C. Williams, and C. Wikström. Concurrent Programming in Erlang. Prentice Hall International, 2nd edition, 1996.
T. Arts and C. Benac Earle. Development of a verified distributed resource locker, In Proc. of FMICS, Paris, July 2001.
T. Arts, M. Dam, L-Å. Fredlund, and D. Gurov. System Description: Verification of Distributed Erlang Programs. In Proc. of CADE’98, LNAI 1421, p. 38–42, Springer-Verlag, Berlin, 1998.
T. Arts and T. Noll. Verifying Generic Erlang Client-Server Implementations. In Proc. of IFL2000, LNCS 2011, p. 37–53, Springer Verlag, Berlin, 2000.
S. Blau and J. Rooth. AXD 301-A new Generation ATM Switching System. Ericsson Review, no 1, 1998.
B. Bollig, M. Leucker, and M. Weber. Local Parallel Model Checking for the Alternation Free μ-Calculus. tech. rep. AIB-04-2001, RWTH Aachen, 2001.
E.M. Clarke, O. Grumberg, D. Peled. Model Checking, MIT Press, December 1999.
J. Corbett, M. Dwyer, L. Hatcliff. Bandera: A Source-level Interface for Model Checking Java Programs. In Teaching and Research Demos at ICSE’00, Limerick, Ireland, 4–11 June, 2000.
CWI. http://www.cwi.nl/~mcrl. A Language and Tool Set to Study Communicating Processes with Data, February 1999.
E. W. Dijkstra. Solution of a Problem in Concurrent Programming Control. In Comm. ACM, 8/9, 1965.
E.A. Emerson and C-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus, In Proc. of the 1st LICS, p. 267–278, 1986.
Open Source Erlang. http://www.erlang.org, 1999.
L-Å. Fredlund, et. al. A Tool for Verifying Software Written in Erlang, To appear in: STTT, 2002.
J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireau. Cadp (Cæsar/Aldébaran development package): A protocol validation and verification toolbox. In Proc. of CAV, LNCS 1102, p. 437–440, Springer-Verlag, Berlin, 1996.
J. F. Groote, The syntax and semantics of timed μCRL. Technical Report SEN-R9709, CWI, June 1997. Available from http://www.cwi.nl.
K. Havelund and T. Pressburger, Model checking Java programs using Java PathFinder. STTT, Vol 2, Nr 4, pp. 366–381, March 2000.
G. Holzmann, The Design and Validation of Computer Protocols. Edgewood Cliffs, MA: Pretence Hall, 1991.
F. Huch, Verification of Erlang Programs using Abstract Interpretation and Model Checking. In Proc. of ICFP’99, Sept. 1999.
D. E. Knuth. Additional Comments on a Problem in Concurrent Programming Control. In Comm. ACM, 9/5, 1966.
D. Kozen. Results on the propositional μ-calculus. TCS, 27:333–354, 1983.
L. Lamport. The Mutual Exclusion Problem Part II-Statement and Solutions. In Journal of the ACM, 33/2, 1986.
N. A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, Inc. San Francisco, California, 1996.
R. Milner. A Calculus of Communicating Systems, Springer 1980.
A. G. Wouters. Manual for the μCRL tool set (version 2.8.2). Tech. Rep. SEN-R0130, CWI, Amsterdam, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arts, T., Earle, C.B., Derrick, J. (2002). Verifying Erlang Code: A Resource Locker Case-Study. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_11
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive