Database of Case Studies Achieved Using CADP

Model-Checking Erlang

Organisation: University of Sheffield (UNITED KINGDOM)
Universidad Politecnica de Madrid (SPAIN)

Method: mCRL2

Tools used: CADP (Construction and Analysis of Distributed Processes)
McErlang

Domain: Telecommunications.

Period: 2010

Size: 5 clients, 1,801,308 states

Description: The Erlang programming language is widely used, particularly in the telecommunications field, for distributed, real-time applications with a high degree of concurrency. This case study uses a distributed and concurrent telecoms example constructed using Erlang and the Open Telecom Platform (OTP) to compare two methods for model checking Erlang applications, McErlang and Etomcrl2/CADP. Etomcrl2 translates the Erlang program into an mCRL2 specification that is model checked using the EVALUATOR tool of CADP. McErlang acts on an Erlang function and uses a monitor call-back module to verify a behavioural safety property, or can model check against a Linear Temporal Logic (LTL) formula using an external standard model checker (which could be CADP).

Two sets of experiments were carried out, property checking and fault detection. Both methods were effective in checking system properties. Both methods isolated the faults, distinguishing between fault implementation and design errors. However, McErlang was not able to verify properties related to timing. The usability of both methods was also assessed.

Conclusions: Both McErlang and Etomcrl2/CADP provide adequate model checking for Erlang programs. McErlang cannot be used to verify properties related to timing, and while it can be used independently to verify behavioural properties, it also requires use of an external model checker to check against an LTL formula. Etomcrl2 requires the entire application, including components of the OTP, to be modeled in mCRL2. This effort pays off by opening up the possibility of using the power of CADP to model check many aspects of the application, and the knowledge gained can be applied in many other fields beyond the focus of Erlang.

Publications: [Guo-Derrick-Earle-Fredlund-10] Qiang Guo, John Derrick, Clara Benac Earle, and Lars-Ake Fredlund. "Model-Checking Erlang - A Comparison between EtomCRL2 and McErlang". Proceedings of the 5th International Academic and Industrial Conference on Testing - Practice and Research Techniques TAIC PART 2010, Lecture Notes in Computer Science vol. 6303, pages 23-38. Springer Verlag, September 2010.
Available on-line at: http://www.springerlink.com/content/bl6961p7tk36g367/
or from our FTP site in PDF and in PostScript

[Guo-Derrick-11] Qiang Guo and John Derrick. "Formally based tool support for model checking Erlang applications." International Journal on Software Tools for Technology Transfer (STTT), 2011:13(4), pages 355-376, August 2011. Available on-line at: http://www.springerlink.com/content/q01r2156p7438213/
Contact:
Qiang Guo
Department of Computer Science
The University of Sheffield
Regent Court
211 Portobello
S1 4DP
UNITED KINGDOM
Email: Q.Guo@dcs.shef.ac.uk



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page