We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Formally based tool support for model checking Erlang applications.
- Authors
Guo, Qiang; Derrick, John
- Abstract
Model checking as a verification technique has proved effective at the system design and hardware level, and is now beginning to be applied to program code. In this paper, we study the application of model checking techniques in the development of Erlang systems. Erlang is a concurrent functional language with specific support for the development of distributed, fault-tolerant systems with soft real-time requirements. It was designed from the start to support a concurrency-oriented programming paradigm and large distributed implementations that this supports. The methodology we describe in this paper consists of abstracting the behaviour of Erlang and OTP components into a process algebraic specification, specifically an mCRL2 specification, upon which the standard model checker CADP can be used to verify the system's properties. In addition to rules that model the Erlang syntax, a translation mechanism for the OTP modules gen_server, supervisor and gen_fsm, and the timeout event are defined. A tool-set etomcrl2 has been developed to automate the process of translation. A small illustrative example is used to evaluate the effectiveness of the proposed techniques, and its results show that the proposed techniques are effective in both verifying properties as well as distinguishing between correct and faulty implementations of the design.
- Subjects
ERLANG (Computer program language); COMPUTER programming; SYSTEMS design; METHODOLOGY; SYSTEMS development; REAL-time clocks (Computers)
- Publication
International Journal on Software Tools for Technology Transfer, 2011, Vol 13, Issue 4, p355
- ISSN
1433-2779
- Publication type
Article
- DOI
10.1007/s10009-010-0179-1