事件B模型的并发调度
Concurrent Scheduling of Event-B Models
摘要：
Event-B是一种基于精化的形式化方法，已被证明在开发并发和分布式程序中非常有用。大型模型可以分解为子模型，这些子模型可以半独立地细化并并行执行。在本文中，我们展示了如何引入显式控制流的并发子模型的事件调度的形式。我们将探讨如何设计时间表，使其应用程序的结果在一个正确的保持细化步骤。为便于实际应用，本文提出了两种引入时间表的模式，以及相应的证明义务。我们证明了我们的方法，将其应用于哲学家用餐问题。
英文摘要：
Event-B is a refinement-based formal method that has been shown to be useful in developing concurrent and distributed programs. Large 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. We explore how schedules can be designed so that their application results in a correctness-preserving refinement step. For practical application, two patterns for schedule introduction are provided, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
