Development of a verified Erlang program for resource locking
Development of a verified Erlang program for resource locking
复制标题
开发经过验证的 Erlang 资源锁定程序
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
J. Derrick
中科院分区：
文献类型：
--
作者：
T. Arts;Clara Benac Earle;J. Derrick
在本文中，我们描述了一种工具，通过工业案例研究来验证Erlang程序，并显示该工具的使用方式。检查组件。 ERLANG建立在软件设计模式的基础上，例如客户 - 服务器行为。凯撒/aldébaran工具集。当一个案例研究中，我们关注的是在AXD 301 ATM开关的控制软件中建模的简化资源管理器。我们为该程序进行了验证的属性是相互排除的，因为该工具集仅支持常规的无替代μ-calculus，因此需要一些固定性来检查案例“非饥饿”。逐步提供更多功能，每个步骤都以使用模型检查相应的正式验证进行动机。
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 .