A Stepwise Development of the Peterson's Mutual Exclusion Algorithm Using B Abstract Systems
A Stepwise Development of the Peterson's Mutual Exclusion Algorithm Using B Abstract Systems
复制标题
使用B抽象系统逐步开发Peterson互斥算法
DOI：
10.1007/11415787_8
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Attiogbé
中科院分区：
文献类型：
--
作者：
J. Attiogbé
我们使用事件 B 提出了 Peterson 互斥算法的逐步正式开发。我们使用自下而上的方法，引入了单独指定的子系统的并行组合。首先，我们将子系统指定为B抽象系统；然后我们组合子系统以获得互斥的第一个抽象解决方案。对该解进行改进以获得Peterson算法。这是通过对先前抽象子系统的细化和组合来实现的。因此，结果是在添加到不变量的正确性（安全性）属性的基础上正式证明的。 Atelier B（B证明者）用于完全检查开发情况。
We present a stepwise formal development of the Peterson's mutual exclusion algorithm using Event B. We use a bottom-up approach where we introduce the parallel composition of subsystems which are separately specified. First, we specify subsystems as B abstract systems; then we compose the subsystems to get a first abstract solution for the mutual exclusion. This solution is improved to obtain the Peterson's algorithm. This is achieved by refinement and composition of the former abstract subsystems. Therefore the result is formally proved on the basis of correctness (safety) properties added to the invariant. Atelier B (a B prover) is used to check completely the development.