|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web 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 |
Back to the CADP case studies page