Development of a Verified Erlang Program for Resource Locking

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 .