D23 Decomposition: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
 
(39 intermediate revisions by 4 users not shown)
Line 1: Line 1:
= Overview =
The Event-B model decomposition is a new feature in the Rodin platform.
Two methods have been identified in the DEPLOY project for model decomposition: the ''shared variable'' decomposition (or A-style decomposition), and the ''shared event'' decomposition (or B-style decomposition). They both answer to the same requirement, namely the possibility to decompose a model <math>M</math> into several independent sub-models <math>M_1, ...,M_n</math>.
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specification and development of model decomposition. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible for the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.
= Motivations =
= Motivations =
{{TODO}}
One of the most important feature of the Event-B approach is the possibility to introduce additional details such as new events and data during refinement steps.
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
Therefore, the refinement process entails an increasing complexity of a model, where one has to deal with a growing number of events, state variables, and consequently proof obligations.
Problem: increasing complexity of the refinement process when having to deal with many events and many state variables (and likely many POs)
This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf Experiences with a Quite Big Event-B Model].


Possible solution: Decomposition
The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. 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 <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>.
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.
The model decomposition leads to some interesting benefits:
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.).  
* 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.


Main benefits:
Note that the possibility of team development is among the current priorities for all industrial partners. The model decomposition is a first answer to this issue.
*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 =
= Choices / Decisions =
{{TODO}}
The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' and ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model, e.g., the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems.
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.  
 
Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (in the DEPLOY description of work, the decomposition support is planned for end of 2009).  
* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).
* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (e.g., the static checker, the proof obligation generator and the editor have been extended).
* Performance. The decomposition tool should perform in reasonable time and memory, compared to other Rodin plug-ins.
* Recursivity. It must be possible to decompose a previously decomposed model.
 
Other technical decisions are justified in the specification wiki pages.


= Available Documentation =
= Available Documentation =
{{TODO}}
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:  
* Event model decomposition specification.
:See [http://wiki.event-b.org/index.php/Event_Model_Decomposition Event Model Decomposition].
* Decomposition plug-in user's guide.
:See [http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide Decomposition Plug-in User Guide].


*Requirements.
= Planning =
*Pre-studies (states of the art, proposals, discussions).  
The decomposition plug-in has been available since release 1.2 of the platform (initial version).
*Technical details (specifications).  
 
*Teaching materials (tutorials).  
A further version allowing to edit an existing decomposition configuration is planned with release 1.3 of the platform.
*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.  
:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].


= Planning =
[[Category:D23 Deliverable]]
The decomposition plug-in is available since release 1.2 of the platform.

Latest revision as of 13:27, 27 January 2010

Overview

The Event-B model decomposition is a new feature in the Rodin platform.

Two methods have been identified in the DEPLOY project for model decomposition: the shared variable decomposition (or A-style decomposition), and the shared event decomposition (or B-style decomposition). They both answer to the same requirement, namely the possibility to decompose a model M into several independent sub-models M_1, ...,M_n.

Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specification and development of model decomposition. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible for the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.

Motivations

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

Therefore, the refinement process entails an increasing complexity of a model, where one has to deal with a growing number of events, state variables, and consequently proof obligations. This is well illustrated in the Event build-up slide of the Wright presentation during the Rodin Workshop 2009.

See Experiences with a Quite Big Event-B Model.

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.

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 priorities for all industrial partners. The model decomposition is a first answer to this issue.

Choices / Decisions

The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (shared variables and shared events) through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model, e.g., the shared variables approach seems more suitable when modelling parallel system and the shared events approach seems more suitable when modelling message-passing distributed systems.

Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:

  • Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (in the DEPLOY description of work, the decomposition support is planned for end of 2009).
  • Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a Tips and Tricks section).
  • Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (e.g., the static checker, the proof obligation generator and the editor have been extended).
  • Performance. The decomposition tool should perform in reasonable time and memory, compared to other Rodin plug-ins.
  • Recursivity. It must be possible to decompose a previously decomposed model.

Other technical decisions are justified in the specification wiki pages.

Available Documentation

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

  • Event model decomposition specification.
See Event Model Decomposition.
  • Decomposition plug-in user's guide.
See Decomposition Plug-in User Guide.

Planning

The decomposition plug-in has been available since release 1.2 of the platform (initial version).

A further version allowing to edit an existing decomposition configuration is planned with release 1.3 of the platform.

See Rodin Platform 1.2 Release Notes and Decomposition Release History.