Skip to main content
Kent Academic Repository

Development of a Verified Erlang Program for Resource Locking

Arts, Thomas, Earle, Clara Benac, 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. (doi:10.1007/s10009-003-0114-9) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:13984)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
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
DOI/Identification number: 10.1007/s10009-003-0114-9
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01 UTC
Last Modified: 16 Nov 2021 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/13984 (The current URI for this page, for reference purposes)

University of Kent Author Information

Derrick, John.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.