Formal Analysis of Erlang's Open Telecom Platform Library Components

Organisation:	University of Sheffield (UNITED KINGDOM)
Method:	Erlang
Tools used:	etomcrl μCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2007
Size:	n/a
Description:	The concurrent functional programming language Erlang explicitly supports real-time and fault-tolerant distributed systems. Associated to Erlang is the OTP (Open Telecom Platform) library providing design patterns offering a solution to a particular class of problems, such as generic server processes, supervisor processes, and finite state machines (the three of which account for around 80% of OTP compliant code). Each design pattern consists of two parts: a generic part implemented in the library and a specific part to be implemented by the programmer (i.e., the user of the design pattern). This case study describes the formal analysis of Erlang programs using the finite state machine design pattern provided by OTP, which allows to represent a finite state machine by a set of transition functions. For each transition, a timeout might be defined. In a first step, the finite state machine is translated into a process algebraic description (in μCRL), the challenge of this translation being to faithfully handle the parameter passing of Erlang, the component mechanism of OTP, the abstraction level, and the timeout mechanism. The former three are achieved by translating the state function in two parts, namely a state process (managing the global variable corresponding to the state) and a set of state functions (encoding the transitions). To handle timeouts, an explicit discrete timing model is introduced by means of tick events. In a second step, the EVALUATOR tool of CADP is used to check safety and liveness properties on the generated process algebraic description. The approach is illustrated on two examples, a door with a code lock and a coffee machine. Six μ-calculus formulas are checked, expressing safety (e.g., "without receiving a correct password, the door cannot be opened") and liveness properties (e.g., "after cappuccino is selected, its price will be displayed").
Conclusions:	The formal analysis tools provided by CADP enable the verification of distributed fault-tolerant Erlang programs following the design patterns provided by the OTP component library.
Publications:	[Guo-07] Qiang Guo. "Verifying Erlang/OTP Components in μCRL". In Proceedings of the 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2007 (Tallinn, Estonia), Lecture Notes in Computer Science, vol. 4574, pp. 227-246, Springer Verlag, June 2007. Available on-line at: http://www.dcs.shef.ac.uk/~qiang/mypapers/Erlang_component_muCRL.pdf or from the CADP Web site in PDF or PostScript [Guo-Derrick-07] Qiang Guo and John Derrick. "Verification of Timed Erlang/OTP Components using the Process Algebra μCRL". In Proceedings of the 2007 SIGPLAN Workshop on Erlang, pp. 55-64, October 2007. Available on-line at: http://www.dcs.shef.ac.uk/~qiang/mypapers/Verification_Timed_Erlang.pdf or from the CADP Web site in PDF or PostScript [Guo-Derrick-Hoch-08] Qiang Guo, John Derrick, and Csaba Hoch. "Verifying Erlang Telecommunication Systems with the Process Algebra μCRL". In Kenji Suzuki, Teruo Higashino, Keiichi Yasumoto, and Khaled El-Fakih editors, Proceedings of the 28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2008 (Tokyo, Japan), Lecture Notes in Computer Science, volume 5048, pp. 201-217, June 2008. Available on-line at: http://www.dcs.shef.ac.uk/~qiang/mypapers/Erlang_Telecomm_muCRL.pdf or from the CADP Web site in PDF or PostScript
Contact:	Prof. John Derrick Department of Computer Science University of Sheffield Regent Court, 211 Portobello St., Sheffield S1 4DP United Kingdom Tel: +44 (0)114 22 21849 Fax: +44 (0)114 22 21810 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