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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Alexili
m
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
The purpose of the platform corrective and evolutive maintenance is to address bugs and feature requests reported either by mail or through the appropriate trackers on SourceForge.
+
Modularisation Plugin realises a support for structuring Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plugin would complement the functionality A/B-style decomposition plugin.
  
The noticeable new features in the main platform for the past year are listed below:
+
The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plugin follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.
* Mathematical Language V2 (releases 1.0 and upper)
 
: The new version of the mathematical language is supported.
 
: See [http://wiki.event-b.org/index.php/Event-B_Mathematical_Language Event-B Mathematical Language].
 
* Theorems everywhere (releases 1.0 and upper)
 
: It is possible to mix theorems and regular predicates in axioms, invariants and guards.
 
* Auto-completion (releases 1.0 and upper)
 
: When entering a predicate or expression in the Event-B machine / context editor, it is possible to type <tt>C-Space</tt> to see a list of possible identifiers that could be entered at the cursor position.
 
* Entering mathematical symbols (releases 1.1 and upper)
 
: The Rodin platform provides many more ways to enter mathematical symbols:
 
: - either type the ASCII shortcut (as in previous releases),
 
: - or type the LaTeX command (as defined in style <tt>bsymb</tt>),
 
: - or click in the ''Symbol Table'' view which displays the symbols graphically,
 
: - or directly enter the Unicode value of the symbol (for advanced users).
 
: See [http://wiki.event-b.org/index.php/Rodin_Keyboard Rodin Keyboard].
 
  
See the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
+
The plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.  
  
 
= Motivations =
 
= Motivations =
The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY 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 [[#Available documentation | trackers]]. Depending on the category, the bug / feature is assigned to the WP9 partner who is in charge of its treatment:
+
There are several conceptual approaches to decomposition. To contrast our proposal, let us consider some of them.
{{SimpleHeader}}
 
|-
 
! scope=col | 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
 
|}
 
  
The priorities are discussed during the WP9 meetings (a management conference call is planned every two weeks, and the WP9 meetings are organised during the DEPLOY workshops).
+
One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.
 +
 
 +
Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity  of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.
 +
 
 +
Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-conatined modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.
 +
 
 +
Modularisation plugin realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:
 +
 
 +
* Structuring large specifications: it is difficult to read and edit large model; there is also a limit to the size of model that the Platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
 +
* Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes. 
 +
* Team development: large models may only be developed by a (often distributed) developers team.
 +
* Model reuse: modules may be exchange and reused in different projects. The notion of interface make it easier to integrate a module in a new context.
 +
* Connection to library components
 +
* Code generation/legacy code
  
 
= Choices / Decisions =
 
= Choices / Decisions =
The WP9 partners have agreed on a release policy (see the [[#Available%20Documentation | Rodin Platform Releases]] wiki page). In particular:
 
* A new version of the Rodin platform is released every 3 months.
 
* The code is frozen during the 2 weeks preceding each release.
 
* The Eclipse versioning policy is enforced (See [http://wiki.eclipse.org/index.php/Version_Numbering http://wiki.eclipse.org/index.php/Version_Numbering]).
 
* A wiki page is dedicated to each release.
 
  
The main advantages, for both developers and end-users, are summarized below:
+
The pimary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount. 
* Information. The wiki page dedicated to each release provides instant information on the new features and improvements, which may be discussed if necessary.
+
 
* Validation. The period of code freeze is more especially devoted to bug fixes, and the frequency of the stable releases is ensured.
+
* We have decided there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than an implicit one such as in A-style decomposition) facilitates reuse of modules and makes it easier to provider a rich management infrastructure.
* Integration. A synchronization between the optional plug-ins and other plug-ins is now possible.
+
 
 +
* At some we had to make a decision of whether to make module integration more explicit and flexible or hide details under syntax sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs any easier.
 +
 
 +
* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.
 +
 
 +
* One crucial point was realising modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implemenation (module body) is a machine and thus it is self-similar to a caller context that is a machine.
 +
 
 +
* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the Platform core.  
  
 
= Available Documentation =
 
= 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 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 =
+
There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.
The [[#Available%20Documentation | Rodin Platform Releases]] wiki page lists in particular the upcoming releases and give the scheduled release dates.
+
 
 +
* [[Plugin wiki|Modularisation Plug-in]]
 +
* [[Plugin tutorial|Modularisation Plug-in Tutorial]]
 +
* [[Installation guide|Modularisation Plug-in Installation Instructions]]
  
Special efforts will be made on the following topics:
 
* Team-based development.
 
: The purpose is to perform simultaneous developments.
 
: In order to understand the problem properly, some usage scenarios (see [http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development http://wiki.event-b.org/index.php/Scenarios_for_Team-based_Development]) for team-based Development have already been written, and a page has also been started to express merging proofs scenarios (see [http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs http://wiki.event-b.org/index.php/Scenarios_for_Merging_Proofs]).
 
: A prototype plug-in is available, which enables the use of the EMF compare editor for machines and contexts. The DEPLOY partners will try out this plug-in and gather requirements for the teamwork plug-in.
 
: See [http://wiki.event-b.org/index.php/EMF_Compare_Editor_Investigation http://wiki.event-b.org/index.php/EMF_Compare_Editor_Investigation] (Implementation issues).
 
: See [http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation http://wiki.event-b.org/index.php/EMF_Compare_Editor_installation] (How to install the EMF Compare editor).
 
: See [http://wiki.event-b.org/index.php/Teamwork_Requirements http://wiki.event-b.org/index.php/Teamwork_Requirements] (Feedback page / Requirements).
 
  
* Documentation.
+
Two small-scale examples are available:
: The purpose is to continuously increase the available documentation on the Wiki. It may contains requirements, pre-studies (states of the art, proposals, discussions), technical details (specifications), teaching materials (tutorials), user's guides, etc. The intended audience may be the developers or the end-users.
+
* [[http://iliasov.org/modplugin/ticketmachine.zip]] - a model of queue based on two ticket machine module instantiations (very basic)
 +
* [[http://iliasov.org/modplugin/doors.zip]] - two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)
  
 +
= Planning =
 
[[Category:D23 Deliverable]]
 
[[Category:D23 Deliverable]]

Revision as of 10:25, 18 November 2009

Overview

Modularisation Plugin realises a support for structuring Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plugin would complement the functionality A/B-style decomposition plugin.

The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plugin follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.

The plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.

Motivations

There are several conceptual approaches to decomposition. To contrast our proposal, let us consider some of them.

One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.

Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.

Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-conatined modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.

Modularisation plugin realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:

  • Structuring large specifications: it is difficult to read and edit large model; there is also a limit to the size of model that the Platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
  • Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes.
  • Team development: large models may only be developed by a (often distributed) developers team.
  • Model reuse: modules may be exchange and reused in different projects. The notion of interface make it easier to integrate a module in a new context.
  • Connection to library components
  • Code generation/legacy code

Choices / Decisions

The pimary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.

  • We have decided there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than an implicit one such as in A-style decomposition) facilitates reuse of modules and makes it easier to provider a rich management infrastructure.
  • At some we had to make a decision of whether to make module integration more explicit and flexible or hide details under syntax sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs any easier.
  • During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.
  • One crucial point was realising modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implemenation (module body) is a machine and thus it is self-similar to a caller context that is a machine.
  • For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the Platform core.

Available Documentation

There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.


Two small-scale examples are available:

  • [[1]] - a model of queue based on two ticket machine module instantiations (very basic)
  • [[2]] - two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)

Planning