Difference between pages "Creating a new plug-in using eclipse (How to extend Rodin Tutorial)" and "D23 Decomposition"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Pascal
 
Line 1: Line 1:
{{Navigation|Previous= [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]]}}
+
= Overview =
 +
The Event-B model decomposition is a new feature in the Rodin platform.
  
=== In this part ===
+
Two methods have been identified in the DEPLOY project for model decomposition: the ''shared variable'' decomposition (or A-style decomposition, after Abrial), and the ''shared event'' decomposition (or B-style decomposition, after Butler). 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>.
* We will explain how to use Eclipse to easily create a plugin package structure for our implementation. Developers which are familiar with plugin building may skip this part and go to the next page of this tutorial.
 
Before starting to perform the following step, you should have your development environment ready and open.
 
  
=== Step 1 ===
+
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specifications and developments. Systerel was more especially responsible of the A-style decomposition. The University of Southampton was in charge of the B-style decomposition.  
To create a plugin, go to "'''File > New > Other'''" and select  "'''Plug-in Project'''" either from the general list if it appears, or from the category "Plug-in Development".
 
Click on "'''Next'''".
 
  
[[Image:Extend_Rodin_Tuto_1_1_File_new_plugin.png|300px]]
+
= 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.
  
=== Step 2 ===
+
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.
The following wizard page appears:
+
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 http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf].
  
[[Image:Extend_Rodin_Tuto_1_2_NewPlug-inProject.png|400px]]
+
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>.
  
1. In project name, enter the name of the plugin package that must appear in the project hierarchy. We used <tt>fr.systerel.rodinextension.sample</tt> but the formalism used often corresponds to <tt>mydomain.mycompany.mypluginname</tt>
+
The model decomposition leads to some interesting benefits:
2. Verify that the plugin is targeted to run with Eclipse 3.6 and click on "'''Next'''".
+
* 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.
  
=== Step 3 ===
+
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.
[[Image:Extend_Rodin_Tuto_1_3_NewPlug-inProject_Content.png|400px]]
 
  
1. In field ID, enter the unique id that will identify the plugin. Generally, we use the project name entered in the previous step : <tt>fr.systerel.rodinextension.sample</tt>,
+
= Choices / Decisions =
2. The version identify, the current plugin version. This field can be later updated via the MANIFEST file. We let the default value <tt>1.0.0.qualifier</tt>,
+
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'' vs. ''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 (eg. 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).
3. In the field Name, put the name of the plugin, here Qualitative Probabilistic Reasoning Plugin,
 
4. In the provider field, you can put the name of your company or insitution,
 
5. Ensure that the Execution Environment used is Java 1.6 (the one used by the Rodin Platform v.2.0),
 
6. Enter the class name of the plugin activator, preceded by its containing package. The activator is the static class responsible of the plugin lifecycle (start, stop, etc.).
 
7. Click on "'''Finish'''"
 
  
=== What we got ===
+
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:
[[Image:Extend_Rodin_Tuto_1_4_ProjectExplorer1.png]]
+
* 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 (according to the DEPLOY description of work, the decomposition support was expected by the end of 2009).
Eclipse created the plugin structure that we will be able to use to extend Rodin.
+
* 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 (eg. the static checker, the proof obligation generator and the editor have been extended).
 +
* Performance.
 +
* Recursivity. Thus, it is possible to decompose a previously decomposed model.
  
{{Navigation|Previous= [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|Extend the database]]}}
+
Other technical decisions are justified in the specification wiki pages.
  
[[Category:Developer documentation|*Index]]
+
= Available Documentation =
[[Category:Rodin Platform|*Index]]
+
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
[[Category:Tutorial|*Index]]
+
* Shared variables (A-style) decomposition specification.
 +
:See [[Event_Model_Decomposition | http://wiki.event-b.org/index.php/Event_Model_Decomposition]].
 +
* Decomposition plug-in user's guide.
 +
:See [[Decomposition_Plug-in_User's_Guide | 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 [[Rodin_Platform_1.2_Release_Notes | http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes]].

Revision as of 15:18, 10 November 2009

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, after Abrial), and the shared event decomposition (or B-style decomposition, after Butler). 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 specifications and developments. Systerel was more especially responsible of the A-style decomposition. The University of Southampton 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 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.

See http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf.

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 vs. 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 (eg. 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 (according to the DEPLOY description of work, the decomposition support was expected by the 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 (eg. the static checker, the proof obligation generator and the editor have been extended).
  • Performance.
  • Recursivity. Thus, it is 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:

  • 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.