Difference between pages "D23 Decomposition" and "D23 Flow Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
(→‎Planning: Added 1,.3 release)
 
imported>Alexili
m (New page: = Overview = Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ...)
 
Line 1: Line 1:
 
= Overview =
 
= 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>.
+
Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows plugin addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.
  
−
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.
+
Sequential composition of events may be expressed in a number of ways:
 +
* event immediately follows another event; no other events may take place between the composed events.
 +
* event eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.
 +
* event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.
 +
 
 +
Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives. Let us see what it means to provide a formal proof for the various cases of sequential event composition.
  
 
= Motivations =
 
= 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 [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf 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 <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>.
 
  
−
The model decomposition leads to some interesting benefits:
+
There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:
−
* 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.
+
* for some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model;
−
* Complexity management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
+
* explicit control flow may help in proving properties related to event ordering;
−
* 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.
+
* sequential code generation requires some form of control flow information;
 +
* since event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information;
 +
* a potential for a visual presentation based on control flow information;
 +
* bridging the gap between high-level workflow and architectural languages, and Event-B.
  
−
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.
+
It is also hoped that the plugin would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.  
  
 
= Choices / Decisions =
 
= 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 =
 
= 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 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].
 
  
 
= Planning =
 
= Planning =
−
The decomposition plug-in has been available since release 1.2 of the platform (initial version).
+
The plugin is to be available for the time of release of Platform version 1.2.
−
 
 
−
A further version allowing to edit an existing decomposition configuration is planned with release 1.3 of the platform.
 
−
 
 
−
: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].
 
  
 
[[Category:D23 Deliverable]]
 
[[Category:D23 Deliverable]]

Revision as of 12:41, 30 November 2009

Overview

Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows plugin addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.

Sequential composition of events may be expressed in a number of ways:

  • event immediately follows another event; no other events may take place between the composed events.
  • event eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.
  • event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.

Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives. Let us see what it means to provide a formal proof for the various cases of sequential event composition.

Motivations

There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:

  • for some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model;
  • explicit control flow may help in proving properties related to event ordering;
  • sequential code generation requires some form of control flow information;
  • since event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information;
  • a potential for a visual presentation based on control flow information;
  • bridging the gap between high-level workflow and architectural languages, and Event-B.

It is also hoped that the plugin would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.

Choices / Decisions

Available Documentation

Planning

The plugin is to be available for the time of release of Platform version 1.2.

Retrieved from ‘https://wiki.event-b.org/index.php?title=D23_Decomposition&oldid=1893’