imported>Pascal |
imported>Fages |
| Line 1: |
Line 1: |
| − | = 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 [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf 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 <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>.
| |
| − |
| |
| − | 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 [[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]]).
| |
