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.

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.