D23 Decomposition

Motivations

TODO This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.

“Top-down” development style: new events and data-refinement of variables during refinements Problem: increasing complexity of the refinement process when having to deal with many events and many state variables (and likely many POs)

Possible solution: Decomposition Cutting a large model into smaller sub-components Shared variables (A-style) vs. Shared events (B-style)

The sub-models M1, ..., Mn can be refined separately and more comfortably than the whole. It should be possible to recomposed the refined models into a single model R in a way that guarantees that R refines M (although never required in practice.).

Main benefits:

• Design/architectural decision (when whole model is not necessarily considered for a given refinement)
• Team development of a model: parts of a decomposed model are shared, allowing independent and parallel developments
• Alleviate the complexity of discharging POs by splitting it over the sub-components

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

TODO This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:

• Requirements.
• Pre-studies (states of the art, proposals, discussions).
• Technical details (specifications).
• Teaching materials (tutorials).
• User's guides.

A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developpers and documentation written for end-users.

Planning

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