Industrial deployment of system engineering methods providing high dependability and productivity


Concurrent Scheduling of Event-B Models

Boström, Pontus and Degerlund, Fredrik and Sere, Kaisa and Waldén, Marina (2011) Concurrent Scheduling of Event-B Models. In: 15th International Refinement Workshop (associated with Formal Methods 2011), 20th June 2011, Limerick, Ireland.

Full text not available from this repository.

Official URL:


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.

Item Type:Conference or Workshop Item (Paper)
Methodology > Refinement
Event-B > Event-B Theory
ID Code:356
Deposited By: Mr. Linas Laibinis
Deposited On:16 Nov 2011 09:32
Last Modified:16 Nov 2011 09:32

Repository Staff Only: item control page

Deploy-Project - All right reserved