D23 Decomposition

Motivations

One of the most important feature of the Event-B approach is the possibility to introduce new events and data-refinement of variables during refinement steps.

It however results in an increasing complexity of the refinement process when having to deal with many events, many state variables, and consequently many proof obligations. This is well illustrated in the Event build-up slide of the Wright presentation during the Rodin Workshop 2009.

The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model $M$ into smaller sub-models $M_1, ..., M_n$. The sub-models can then be refined separately and more comfortably than the whole. The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model $MR$ in a way that guarantees that $MR$ refines $M$.

Two methods have been identified for model decomposition: the shared variable decomposition (or A-style decomposition), and the shared event decomposition (or B-style decomposition). They both answer to this requirement.

The model decomposition leads to some interesting benefits:

• Design/architectural decision. It applies in particular when it is noticed that it is not necessary to consider the whole model for a given refinement step, because only a few events and variables are involved instead.
• Complexity management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
• Team development. More precisely, it gives a way for several developers to share the parts of a decomposed model, and to work independently and possibly in parallel on them.

Note that the possibility of team development is among the current development priorities for all industrial partners. The model decomposition is a first answer to this large problematic.

Choices / Decisions

TODO This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

A single plug-in for both styles in the Rodin platform.

The configuration (i.e. the identification of the machine taken as input for the decomposition, the identification of the sub-machines to be generated and the first step of the decomposition) shall be performed through the Graphical User Interface (GUI) of the Rodin platform. It is indeed more suitable for the end-user to visualize the configuration. In the future the option of using GMF (Graphical Modelling Framework) for the decomposition visualization will be explored.

As far as possible, the developments shall not be performed in the Event- B core: dedicated extension points shall be used instead to keep as much independent as possible from the core.

The created projects and components (machines and contexts) shall be tagged as “automatically generated”.

The non-decomposed model is assumed to be proved.

The decomposition does not generate new POs.

See the specification for technical decisions (eg. events partition is the first step for A-style decomposition).

Available Documentation

The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:

• Shared variables (A-style) decomposition specification.

See http://wiki.event-b.org/index.php/Event_Model_Decomposition.

• Decomposition plug-in user's guide.

See http://wiki.event-b.org/index.php/Decomposition_Plug-in_User's_Guide.

Planning

The decomposition plug-in is available since release 1.2 of the platform.

See http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes).