Development of a Verified Erlang Program for Resource Locking

Arts, Thomas and Earle, Clara Benac and Derrick, John (2003) Development of a Verified Erlang Program for Resource Locking. Software Tools for Technology Transfer (STTT), 5 (2). pp. 205-220. ISSN 1433-2779 . (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/s10009-003-0114-9

Abstract

In this paper, we describe a tool to verify Erlang programs and show, by means of an industrial case study, how this tool is used. The tool includes a number of components, including a translation component, a state space generation component and a model checking component. To verify properties of the code, the tool first translates the Erlang code into a process algebraic specification. The outcome of the translation is made more efficient by taking advantage of the fact that software written in Erlang builds upon software design patterns such as client–server behaviours. A labelled transition system is constructed from the specification by use of the μCRL toolset. The resulting labelled transition system is model checked against a set of properties formulated in the μ-calculus using the Caesar/Aldébaran toolset.As a case study we focus on a simplified resource manager modelled on a real implementation in the control software of the AXD 301 ATM switch. Some of the key properties we verified for the program are mutual exclusion and non-starvation. Since the toolset supports only the regular alternation-free μ-calculus, some ingenuity is needed for checking the liveness property “non-starvation”. The case study has been refined step by step to provide more functionality, with each step motivated by a corresponding formal verification using model checking .

Item Type: Article
Uncontrolled keywords: Formal Methods, Software Verification, Model Checking, Functional Programming, Erlang
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01
Last Modified: 11 Apr 2014 15:30
Resource URI: http://kar.kent.ac.uk/id/eprint/13984 (The current URI for this page, for reference purposes)
  • Depositors only (login required):