Difference between pages "Code Generation Activity" and "D23 Pattern Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Pascal
 
Line 1: Line 1:
−
Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk; Chris Lovell mailto:cjl3@ecs.soton.ac.uk or Renato Silva mailto:ras07r@ecs.soton.ac.uk
+
= Overview =
−
=== Code Generation Feature - Version 0.2.0 For Rodin 2.3===
+
The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.
−
This section is undergoing maintenance. We have release a new version of the code generator on 30/11/11, and documentation is being updated where necessary.
 
−
===== Changes to the Tooling and Approach =====
 
−
The main changes are:
 
−
* The code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
 
−
* Tasking Event-B is now integrated with the Event-B explorer.
 
−
* The Rose Editor is used for editing the Tasking Event-B, and
 
−
* a text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
 
−
* The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
 
−
* Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
 
−
* The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
 
−
* The translation of target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
 
−
* Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
 
−
* The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
 
  
−
===== Changes to the Documentation =====
+
A refinement can also be seen as the solution to the problem encountered in the abstraction. One can make use of such a solution if the solved problem appears in the current development. Instead of solving the problem again we directly use the already known solution. Certainly, we have to show that our current problem (or at least part of it) is the same as the solved problem.
−
The following Pages have been updated:
 
−
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview Tasking Event-B Overview]
 
−
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Tutorial Tutorial]
 
  
−
===== Downloads =====
+
We refer to such a reusable model containing a certain solution to a problem as a pattern. Since these patterns are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model (solved problem).
−
* The Code Generation feature is available by accessing the main Rodin Update Site. In Eclispe click on Help/Install new Software. Find the Rodin update site from the list. In Utilities add Code Generation.
 
−
*The approach makes use of the following:
 
−
**Model Decomposition: Download from the main Rodin Update Site, in the Decomposition section.
 
−
**Shared Event Decomposition: Download from the main Rodin Update Site, in the Decomposition section.
 
−
**Theory Plug-in: Download from the main Rodin Update Site, in the Utilities section.
 
  
−
+
As mentioned above, the problem at hand (or at least part of it) has to be similar to the pattern we want to use. To ensure this similarity the developer has to match the pattern with the problem at hand. After a successful matching of the models (problems) the refinement (solution) of the pattern can be incorporated into the problem at hand. This leads to a refinement of this model that is correct by construction. In other words, a new refinement of the problem at hand can be generated which includes the achievements of the pattern and is correct without proving any proof obligation.
−
* Tutorial projects are available from the Examples directory (use v0.2.0) [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd SVN].
 
−
* Sources at: ???
 
  
 +
= Motivations =
 +
The idea of patterns and their usage is described in every detail in the Master Thesis [http://e-collection.ethbib.ethz.ch/view/eth:41612 "Design Patterns in Event-B and Their Tool Support“]. This approach follows the earlier proposal of Jean-Raymond Abrial and Thai Son Hoang stated in the paper [http://www.springerlink.com/content/d088h53531x7226j "Using Design Patterns in Formal Methods: An Event-B Approach"].
  
−
TODO
+
There are two main motivations to use patterns.
−
* Add array types.
 
−
* Add addressed variables (for direct read/write access to memory)
 
−
* Flattening of composed machines/implementation machines.
 
−
* Interrupts
 
  
−
=== Sensing and Actuating for Tasking Event-B ===
+
*Reusing solutions to problems:
−
Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
 
  
−
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
+
:Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting in this "best" solution one does not have to bother finding it ever again.
  
−
* As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu ''help/install new software'': http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
*Reusing proofs:
  
−
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
:As mentioned above, the pattern approach is able to generate a refinement that is correct by construction. This is possible because the construction of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.
  
−
A new [http://wiki.event-b.org/index.php?title=Tasking_Event-B_Tutorial Code Generation Tutorial] has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
+
Case studies showed also another motivation to have such a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.
  
−
The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive] or [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
+
= Choices / Decisions =
 +
*To support the developer and guide him through the whole pattern process, we designed a plug-in providing a graphical wizard that consists in several pages, one for each major step.
  
−
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
*It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programmatically. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.
  
−
Released 24 January 2011.
+
*In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).
  
−
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
*The correctness of the matching, which is checking the syntactical equality of the matched elements (guards, actions) is left to the developer for the moment. The automation of this was postponed to a later version as it appears to us as a minor point.
  
−
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
*As the pattern plug-in is in a pre-release phase, there is an option to generate the proof obligation in order to control the generation.
  
−
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
= Available Documentation =
 +
Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.
  
−
The code generation tutorial examples are available for download at:
+
:See [http://wiki.event-b.org/index.php/Pattern Pattern] for a short overview of the idea of patterns in Event-B and stepwise instructions for both developers interested in using the wizard and those more thrilled by APIs.
  
−
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
= Planning =
  
−
The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at:
+
The pattern tool is available as an external plug-in for Rodin release 1.1 and above.
 +
:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.1_Release_Notes Rodin Platform 1.1 Release Notes] and [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release_Notes].
  
−
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
The current version of the pattern plug-in covers the following functionalities:
 +
* Interactive guidance for matching the variables.
 +
* Interactive guidance for matching the events and their parameters, guards and actions.
 +
* Collecting the seen contexts in order to enable the user to match the carrier sets and constants.
 +
* Checking for name clashes and proposing possible renaming.
 +
* Detection of disappearing variables that have to be replaced.
 +
* Detection of disappearing parameters that have to be replaced.
 +
* Generation of the new machine file.
  
−
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
Desired functionalities that are missing in the current version:
 +
* Automated syntactical check of the matched elements.
 +
* Automated extraction of the glueing invariants to find the replacement for disappearing variables.
 +
* Automated extraction of the witnesses to find the replacement for disappearing parameters.
  
−
== Code Generation Status ==
+
The current version has been passed to interested partners for evaluation. The date for the missing functionalities being implemented in the plug-in will depend on the responses of the evaluators and their need of having those functionalities available.
−
=== Latest Developments ===
 
−
* Demonstrator plug-in feature version 0.1.0
 
−
** for Rodin 2.1.x version is available.
 
  
−
* The Code Generation feature consists of,
+
[[Category:D23 Deliverable]]
−
** a tasking Development Generator.
 
−
** a tasking Development Editor (Based on an EMF Tree Editor).
 
−
** a translator, from Tasking Development to Common Language Model (IL1).
 
−
** a translator, from the Tasking Development to Event-B model of the implementation.
 
−
** a pretty-printer for the Tasking Development.
 
−
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
−
 
 
−
* A tutorial is available [[Code Generation Tutorial]]
 
−
** Step 1 - Create the tasking development.
 
−
** Step 2 - Add annotations.
 
−
** Step 3 - Invoke translators.
 
−
 
 
−
=== Ongoing Work ===
 
−
 
 
−
* Full Rodin Integration
 
−
* Sensed Variables
 
−
* Branching in Shared Machines
 
−
 
 
−
=== Future Work ===
 
−
* Support for Interrupts.
 
−
* Richer DataTypes.
 
−
* Accommodation of duplicate event names in tasking developments.
 
−
 
 
−
== Metamodels ==
 
−
* In the plug-in we define several meta-models:
 
−
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
 
−
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.
 
−
** Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
 
−
 
 
−
== Translation Rules ==
 
−
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
 
−
 
 
−
== Release History ==
 
−
=== The Code Generation Demonstrator for Rodin 1.3.x ===
 
−
 
 
−
 
 
−
First release: 30 November 2010.
 
−
 
 
−
available from:
 
−
 
 
−
https://sourceforge.net/projects/codegenerationd/files/
 
−
 
 
−
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.
 
−
 
 
−
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to ''<installPath>\rodin1.3bWin7\workspace''. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
 
−
 
 
−
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.
 
−
 
 
−
'''A step-by-step [[Code Generation Tutorial]] is available'''
 
−
 
 
−
==== About the Initial Release ====
 
−
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.
 
−
 
 
−
==== Source Code ====
 
−
 
 
−
The sources are available from,
 
−
 
 
−
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
 
−
 
 
−
Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0
 
−
 
 
−
 
 
−
 
 
−
[[Category:Work in progress]]
 

Latest revision as of 14:43, 27 January 2010

Overview

The pattern plug-in enables an Event-B developer to make advantage of former models and their refinements.

A refinement can also be seen as the solution to the problem encountered in the abstraction. One can make use of such a solution if the solved problem appears in the current development. Instead of solving the problem again we directly use the already known solution. Certainly, we have to show that our current problem (or at least part of it) is the same as the solved problem.

We refer to such a reusable model containing a certain solution to a problem as a pattern. Since these patterns are just regular models every model can be a pattern in principle. There is only a limit in terms of usability that correlates with the specificity of the model (solved problem).

As mentioned above, the problem at hand (or at least part of it) has to be similar to the pattern we want to use. To ensure this similarity the developer has to match the pattern with the problem at hand. After a successful matching of the models (problems) the refinement (solution) of the pattern can be incorporated into the problem at hand. This leads to a refinement of this model that is correct by construction. In other words, a new refinement of the problem at hand can be generated which includes the achievements of the pattern and is correct without proving any proof obligation.

Motivations

The idea of patterns and their usage is described in every detail in the Master Thesis "Design Patterns in Event-B and Their Tool Support“. This approach follows the earlier proposal of Jean-Raymond Abrial and Thai Son Hoang stated in the paper "Using Design Patterns in Formal Methods: An Event-B Approach".

There are two main motivations to use patterns.

  • Reusing solutions to problems:
Usually there is more than one solution to a problem. But not every solution is of equal quality. There are solutions that are especially easy, elegant or short. For a lot of problems there is a best practice to solve it. Having a pattern consisting in this "best" solution one does not have to bother finding it ever again.
  • Reusing proofs:
As mentioned above, the pattern approach is able to generate a refinement that is correct by construction. This is possible because the construction of the refinement leads to the same proof obligations as in the pattern. Since they are proved in the pattern there is no need do the same proof steps in the current development again. Reusing proofs, especially manual discharged proof obligations, saves a lot of time for the developer. The drawback reflects in the effort to match the pattern with the problem before a refinement can be generated. But this effort can be minimised by a tool that does as many steps as possible automatically or at least supports the developer wherever user interaction is required.

Case studies showed also another motivation to have such a tool. Using the pattern approach without tool support, especially the generation of the refinement, is time consuming and error prone. In this last step in the whole procedure, basically two machines are merged by copying and pasting elements. This often leads to name clashes where a developer can easily loose track. Having a tool checking for possible name clashes in advance can avoid a lot of confusion.

Choices / Decisions

  • To support the developer and guide him through the whole pattern process, we designed a plug-in providing a graphical wizard that consists in several pages, one for each major step.
  • It was desired to have direct access to the pattern plug-in in form of an API in addition to the wizard. This enables other Rodin developers to use the pattern plug-in programmatically. For this, the first version of the plug-in was revised by having the generation apart from the pure graphical interface.
  • In order to speed up the process, all required Event-B element of the involved machines are collected in a central data object. Certain elements are contained in more than one list dependent to their attributes (e.g. a matched and renamed event).
  • The correctness of the matching, which is checking the syntactical equality of the matched elements (guards, actions) is left to the developer for the moment. The automation of this was postponed to a later version as it appears to us as a minor point.
  • As the pattern plug-in is in a pre-release phase, there is an option to generate the proof obligation in order to control the generation.

Available Documentation

Besides the documents mentioned above focusing on the theory there also exists a wiki page that is more tool related.

See Pattern for a short overview of the idea of patterns in Event-B and stepwise instructions for both developers interested in using the wizard and those more thrilled by APIs.

Planning

The pattern tool is available as an external plug-in for Rodin release 1.1 and above.

See Rodin Platform 1.1 Release Notes and Rodin Platform 1.2 Release_Notes.

The current version of the pattern plug-in covers the following functionalities:

  • Interactive guidance for matching the variables.
  • Interactive guidance for matching the events and their parameters, guards and actions.
  • Collecting the seen contexts in order to enable the user to match the carrier sets and constants.
  • Checking for name clashes and proposing possible renaming.
  • Detection of disappearing variables that have to be replaced.
  • Detection of disappearing parameters that have to be replaced.
  • Generation of the new machine file.

Desired functionalities that are missing in the current version:

  • Automated syntactical check of the matched elements.
  • Automated extraction of the glueing invariants to find the replacement for disappearing variables.
  • Automated extraction of the witnesses to find the replacement for disappearing parameters.

The current version has been passed to interested partners for evaluation. The date for the missing functionalities being implemented in the plug-in will depend on the responses of the evaluators and their need of having those functionalities available.

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