Concurrent Scheduling of Event-B Models

TL;DR

This paper presents a method for introducing explicit control flow via event schedules in Event-B models, enabling correct and efficient concurrent execution of sub-models, demonstrated through the dining philosophers problem.

Contribution

It proposes a novel approach to incorporate event schedules into Event-B, ensuring correctness preservation and providing practical patterns with proof obligations.

Findings

Schedules can be designed to preserve correctness during refinement

Two practical patterns for schedule introduction are provided

Application to the dining philosophers problem demonstrates effectiveness

Abstract

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.