Difference between pages "D23 Flow Plug-in" and "D23 General Platform Maintenance"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Alexili
 
imported>Pascal
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
 +
The purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests.
  
−
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.
+
The main evolutions of the Rodin platform are driven by the description of work for the Rodin project and the requirements expressed by industrial WP1 to WP5 partners or by consultants during the lifecycle of the project.
  
−
Sequential composition of events may be expressed in a number of ways:
+
Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platform or request a new feature, using the dedicated trackers. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of its treatment:
−
* event immediately follows another event; no other events may take place between the composed events.
+
{{SimpleHeader}}
−
* 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.
+
! scope=col | Category || Partner
−
 
+
|-
−
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.
+
|AnimB || Christophe METAYER
 +
|-
 +
|B2LaTeX || University of Southampton
 +
|-
 +
|Decomposition || Systerel
 +
|-
 +
|Event-B core || Systerel
 +
|-
 +
|Event-B interface || Systerel
 +
|-
 +
|Event-B POG || Systerel
 +
|-
 +
|Event-B provers || Systerel
 +
|-
 +
|Event-B static checker || Systerel
 +
|-
 +
|PRO-B || Dusseldorf
 +
|-
 +
|Renaming || University of Southampton
 +
|-
 +
|Requirements || Dusseldorf
 +
|-
 +
|Rodin platform || Systerel
 +
|-
 +
|Text editor || Dusseldorf
 +
|-
 +
|U2B || Southampton
 +
|}
  
 
= Motivations =
 
= Motivations =
−
 
+
{{TODO}}
−
There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:
+
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.  
−
* 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 =
 
= Choices / Decisions =
−
 
+
{{TODO}}
−
The primary functionality of the plugin is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plugin and the proof obligations related to flow appear in the list of the model proof obligations.
+
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.  
−
 
 
−
One of the lessons learned with an initial plugin prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are not familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF: an Eclipse library for manipulating EMF models using graphical editors.  
 
  
 
= Available Documentation =
 
= Available Documentation =
−
 
+
The following pages give useful information about the Rodin platform releases:
−
There is a [[Flows|wiki]] page summarising proof obligation involved in proving machine/flow consistency.
+
* Release notes.
 +
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases http://wiki.event-b.org/index.php/Rodin_Platform_Releases].
 +
: More details are provided in the notes distributed with each release (eg. [http://sourceforge.net/project/shownotes.php?release_id=693928 http://sourceforge.net/project/shownotes.php?release_id=693928]).
 +
* Bugs.
 +
: See [http://sourceforge.net/tracker/?atid=651669&group_id=108850 http://sourceforge.net/tracker/?group_id=108850&atid=651669].
 +
* Feature requests.
 +
: See [http://sourceforge.net/tracker/?group_id=108850&atid=651672 http://sourceforge.net/tracker/?group_id=108850&atid=651672].
  
 
= Planning =
 
= Planning =
−
The plugin is to be available for the time of release of Platform version 1.2.
+
The ''Rodin Platform Releases'' wiki page lists in particular the upcoming releases and give the scheduled release dates.
−
 
 
−
[[Category:D23 Deliverable]]
 

Revision as of 17:48, 10 November 2009

Overview

The purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests.

The main evolutions of the Rodin platform are driven by the description of work for the Rodin project and the requirements expressed by industrial WP1 to WP5 partners or by consultants during the lifecycle of the project.

Beyond that, any user registered on SourceForge may record any encountered bug on the Rodin platform or request a new feature, using the dedicated trackers. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of its treatment:

Category Partner
AnimB Christophe METAYER
B2LaTeX University of Southampton
Decomposition Systerel
Event-B core Systerel
Event-B interface Systerel
Event-B POG Systerel
Event-B provers Systerel
Event-B static checker Systerel
PRO-B Dusseldorf
Renaming University of Southampton
Requirements Dusseldorf
Rodin platform Systerel
Text editor Dusseldorf
U2B Southampton

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.

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.

Available Documentation

The following pages give useful information about the Rodin platform releases:

  • Release notes.
See http://wiki.event-b.org/index.php/Rodin_Platform_Releases.
More details are provided in the notes distributed with each release (eg. http://sourceforge.net/project/shownotes.php?release_id=693928).
  • Bugs.
See http://sourceforge.net/tracker/?group_id=108850&atid=651669.
  • Feature requests.
See http://sourceforge.net/tracker/?group_id=108850&atid=651672.

Planning

The Rodin Platform Releases wiki page lists in particular the upcoming releases and give the scheduled release dates.

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