Event Model Decomposition

Introduction

One of the most important feature of the Event-B approach is the ability to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.

The main idea of the decomposition is to cut a model $A$ into sub-models $A_1, ..., A_n$, which can be refined separately and more confortably than the whole.

The constraint that shall be satisfied by the decomposition is that these refined models might - the recomposition will never be performed in practice - be recomposed into a whole model $R$ in a way that guarantees that $R$ refines $A$. An event-based decomposition of a model is detailed in Event Model Decomposition: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events are acting are distributed among the sub_models.

The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.

Bibliography

• J.R. Abrial, Mathematical Models for Refinement and Decomposition, in The Event-B Book, February 2007.
• J.R. Abrial, Event Model Decomposition, Version 1.3, April 2009.
• M. Butler, Decomposition Structures for Event-B, in Integrated Formal Methods iFM2009, Springer, LNCS 5423, 2009 (lien externe).