Derivation of concurrent programs by stepwise scheduling of Event-B models
Derivation of concurrent programs by stepwise scheduling of Event-B models
复制标题
通过Event-B模型的逐步调度推导并发程序
DOI：
--
复制
发表时间：
2012
影响因子：
1
通讯作者：
M. Waldén
中科院分区：
文献类型：
--
作者：
Pontus Boström;Fredrik Degerlund;K. Sere;M. Waldén
并发程序通常是复杂的，它们不容易开发和证明是正确的。基于细化的形式化开发方法不仅可以逐步地推导程序，而且可以逐步地证明它们的正确性。Event-B是一个正式的框架，已被证明对并发和分布式程序的开发非常有用。为了扩展到大型系统，可以将模型分解为子模型，这些子模型可以半独立地进行细化并并行执行。在本文中，我们展示了如何以事件调度的形式为并发子模型引入显式控制流。这些计划的目的是提供面向过程的程序规范，以补充Event-B中基于状态的方法，并促进更有效地实现模型。进度表以一种循序渐进的方式引入，并且应该设计成一个保持正确性的改进步骤。为了减少开发人员的验证负担，我们提供了时间表引入的模式，以及它们相关的证明义务。我们通过将其应用于用餐哲学家问题来证明我们的方法。
Concurrent programs are often complex and they are not straightforward to develop and prove correct. Formal development methods based on refinement make it possible not only to derive programs gradually, but also to prove their correctness in a stepwise fashion. Event-B is a formal framework that has been shown useful for developing concurrent and distributed programs. In order to scale to large systems, models can be decomposed into sub-models that can be refined semi-independently and executed in parallel. In this paper, we show how to introduce explicit control flow for the concurrent sub-models in the form of event schedules. The purpose of these schedules is both to provide process-oriented specifications of the programs to complement the state-based approach in Event-B, as well as to facilitate more efficient implementation of the models. The schedules are introduced in a stepwise manner and should be designed to result in a correctness-preserving refinement step. In order to reduce the verification burden on the developers, we provide patterns for schedule introduction, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.