Difference between pages "ADVANCE D3.2 General Platform Maintenance" and "Code Generation Activity"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>Andy
 
Line 1: Line 1:
−
== Core Rodin platform (Thomas Muller) ==
+
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
 +
=== Code Generation Feature - Version 0.2.0 ===
 +
This section is undergoing maintenance. We are planning to release a new version of the code generator in the next few days.
 +
The main changes are:
 +
* The new 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 TaskBody text-based editor is provided, in Rose, for specifying the flow control. This feature has been added to address some of the usability issues.
 +
* The EMF tree editor in Rose is only used minimally, and we plan further enhancements to reduce this.
 +
* Composed machines are used to store event 'synchronizations'. 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 the mathematical language of target languages, is specified in the Theory plug-in.
 +
* 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.
  
−
=== Overview ===
+
=== Sensing and Actuating for Tasking Event-B ===
−
{{TODO|Fill this paragraph.}}
+
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.
  
−
=== Motivations / Decisions ===
+
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
−
{{TODO|Fill this paragraph.}}
 
  
−
=== Available Documentation ===
+
* 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/
−
{{TODO|Fill this paragraph.}}
 
  
−
=== Planning ===
+
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
−
{{TODO|Fill this paragraph.}}
 
  
 +
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].
  
 +
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].
  
−
== UML-B Improvements (Colin Snook, Vitaly Savicks) ==
+
=== The Code Generation Demonstrator for Rodin 2.1.x ===
  
−
=== Overview ===
+
Released 24 January 2011.
  
−
The UML-B plug-in and associated frameworks are developed and maintained by Dr Colin Snook at the University of Southampton. Significant contributions (to the latest version) have been made by Vitaly Savicks (State-machines) and Gintautas Sulskus (Class Diagrams). The UML-B plugin provides UML-like diagrammatic modelling as an extension to Event-B and the Rodin platform. UML-B is an established plug-in which will be developed and improved to support the aims of the Advance project. UML-B was redeveloped during the Deploy project to provide closer integration with Event-B. A state-machine diagram editor is already released in this integrated version and a class diagram editor is now being developed as a prototype. Other improvements will include new diagrammatic notations which are directly related to the aims of advance, such as component diagrams, as well as more general improvements, such as usability, and any features required by the projects industrial partners.
+
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
  
−
=== Motivations / Decisions ===
+
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
  
−
The implementation of the UML-B tool is structured to provide re-usable features as much as possible. To achieve this, wherever possible, generic frameworks are developed and the implementation of specific diagram tools is minimised by utilising these frameworks. The following frameworks are now in use by UML-B and available as a basis for future diagrammatic modelling notations.
+
The update-site is available through the Rodin update site in the ''Utilities'' category.
  
−
* The Event-B EMF framework provides an EMF basis for Event-B models (developed during the Deploy project).
+
The code generation tutorial examples are available for download at:
−
** Provides an EMF representation of Event-B models with persistance into the Rodin database.
 
−
* The Event-B EMF Support for Modelling Extensions framework provides support for extending Event-B with new modelling features (initially developed during the Deploy project and now being extended in the Advance project).
 
−
** Provides Navigator support for EMF-only model elements
 
−
** Provides a persistence mechanism for model extensions that are not needed to be processed by Rodin.
 
−
** A Generic Refiner for modelling extensions has recently been added.
 
−
* The Event-B GMF Diagrams Generic Support framework provides support for developing new diagram notations (started in the Deploy project but mostly developed during the Advance project).
 
−
** Provides Generic support for diagrammatic aspects of modelling extensions
 
−
** A generic Validation and Event-B generation service has recently been added
 
−
 
−
A new release of the State-machine diagram editor has been made. This release corrected some problems and improved use of the generic framework features.
 
  
−
Work is in progress on a new version of the UML-B Class Diagram editor. This takes the same approach as the State-machines editor in that the models are contained within Machines (and, in this case, also Contexts) and that diagrammatic model features link to and enhance existing Event-B elements rather than generate everything. The Class diagram editor is currently a prototype and has not been released.
+
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
  
−
=== Available Documentation ===
+
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:
  
−
[reference Fontainebleau Rodin workshop paper on Generic frameworks]
+
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
  
−
Wiki pages for developers using the Generic extensions and Diagrams frameworks.
+
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
−
http://wiki.event-b.org/index.php/EMF_framework_for_Event-B
 
−
http://wiki.event-b.org/index.php/Generic_Event-B_EMF_extensions (Under Construction)
 
  
−
[reference Dusseldorf Rodin workshop paper on Event-B Statemachines]
+
== Code Generation Status ==
−
Wiki pages for users of UML-B
+
=== Latest Developments ===
−
http://wiki.event-b.org/index.php/UML-B
+
* Demonstrator plug-in feature version 0.1.0
 +
** for Rodin 2.1.x version is available.
  
−
=== Planning ===
+
* The Code Generation feature consists of,
 +
** 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.
  
−
The following work is planned:
+
* A tutorial is available [[Code Generation Tutorial]]
−
* Re-base the Event-B EMF framework on the EMF model of the Rodin elements which is now available as a result of the development of a new Rodin editor to replace the form based editor.
+
** Step 1 - Create the tasking development.
−
* Re-write the Event-B generator of the State-machine diagram editor so that it uses the generic generator from the Event-B GMF Support for Generic Diagrams framework. This will improve performance as the current QVT based implementation is too slow.
+
** Step 2 - Add annotations.
−
* Improve the State-machine diagram animation interface so that it supports animation of multiple diagrams.
+
** Step 3 - Invoke translators.
−
* Complete the development of the new version of the UML-B Class Diagram editor.  
 
−
* Develop Animation interface for the Class diagram editor.
 
−
* Develop a Component diagram editor and associated simulation tools.
 
  
−
== Code generation (Andy Edmunds) ==
+
=== Ongoing Work ===
  
−
=== Overview ===
+
* Full Rodin Integration
−
{{TODO|Fill this paragraph.}}
+
* Sensed Variables
 +
* Branching in Shared Machines
  
−
=== Motivations / Decisions ===
+
=== Future Work ===
−
{{TODO|Fill this paragraph.}}
+
* Support for Interrupts.
 +
* Richer DataTypes.
 +
* Accommodation of duplicate event names in tasking developments.
  
−
=== Available Documentation ===
+
== Metamodels ==
−
{{TODO|Fill this paragraph.}}
+
* 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.
  
−
=== Planning ===
+
== Translation Rules ==
−
{{TODO|Fill this paragraph.}}
+
* 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 ===
  
  
−
== ProR (Michael Jastram/Lukas Ladenberger) ==
+
First release: 30 November 2010.
  
−
=== Overview ===
+
available from:
  
−
{{TODO|Fill this paragraph.}}
+
https://sourceforge.net/projects/codegenerationd/files/
  
−
* A Method for Tracing Requirements into Specifications
+
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.
−
* ProR/Rodin Integration plugin to support the method
 
  
−
=== Motivations / Decisions ===
+
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.
  
−
{{TODO|Fill this paragraph.}}
+
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.  
  
−
The motivation of the Rodin/ProR integration plugin was to bring two complimentary fields of research, requirements engineering and formal modelling, closer together. Especially, the traceability within a system description is a challenging problem of requirements engineering. In particular, formal models of the system are often based on informal requirements, but creating and maintaining the traceability between the two can be challenging. In <ref name="req1ref">http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref>, we presented an incremental approach for producing a system description from an initial set of requirements. The foundation of the approach is a classification of requirements into artefacts W (domain properties), R (requirements) and S (specification). In addition, the approach uses designated phenomena as the vocabulary employed by the artefacts. The central idea is that adequacy of the system description must be justified, meaning that W ∧ S ⇒ R. The approach establishes a traceability, and the resulting system description may consist of formal and informal artefacts. We created tool support for this approach by integrating Rodin and ProR. We designed it with the goal to support the approach described in <ref name="req1ref"/>, and to ease the integration of natural language requirements and Event-B.
+
'''A step-by-step [[Code Generation Tutorial]] is available'''
  
−
=== Available Documentation ===
+
==== 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.
  
−
{{TODO|Fill this paragraph.}}
+
==== Source Code ====
  
−
* A Method and Tool for Tracing Requirements into Specifications: <ref name="req1ref"/> The paper has been submitted to Science of Computer Programming.
+
The sources are available from,
−
* Requirements Traceability between Textual Requirements and Formal Models Using ProR: <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/LadenbergerJastram_iFMABZ2012</ref> The paper has been accepted for iFM'2012.
 
  
−
* Tutorial for the Rodin/ProR integration can be found here: <ref>http://wiki.event-b.org/index.php/ProR</ref>.
+
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
−
* The User Guide containing an additional Tutorial for ProR can be found here: <ref>http://wiki.eclipse.org/RMF/User_Guide</ref>.
 
  
−
=== Planning ===
+
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
  
−
{{TODO|Fill this paragraph.}}
 
  
−
There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref name="req1ref"/> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.
 
  
−
Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.
+
[[Category:Work in progress]]
−
 
 
−
== References ==
 
−
<references/>
 
−
 
 
−
== Camille (Ingo Weigelt) ==
 
−
 
 
−
=== Overview ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
=== Motivations / Decisions ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
=== Available Documentation ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
=== Planning ===
 
−
{{TODO|Fill this paragraph.}}
 
−
 
 
−
== References ==
 
−
<references/>
 
−
 
 
−
[[Category:ADVANCE D3.2 Deliverable]]
 

Revision as of 15:51, 24 November 2011

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

Code Generation Feature - Version 0.2.0

This section is undergoing maintenance. We are planning to release a new version of the code generator in the next few days. The main changes are:

  • The new 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 TaskBody text-based editor is provided, in Rose, for specifying the flow control. This feature has been added to address some of the usability issues.
  • The EMF tree editor in Rose is only used minimally, and we plan further enhancements to reduce this.
  • Composed machines are used to store event 'synchronizations'. 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 the mathematical language of target languages, is specified in the Theory plug-in.
  • 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.

Sensing and Actuating for Tasking Event-B

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.
  • Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.

A new 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, here.

The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the Deploy E-Prints archive or Examples SVN site.

The Code Generation Demonstrator for Rodin 2.1.x

Released 24 January 2011.

The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at: 

 https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration

The update-site is available through the Rodin update site in the Utilities category.

The code generation tutorial examples are available for download at: 

 https://sourceforge.net/projects/codegenerationd/files/DemoFiles/

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: 

 http://download.eclipse.org/modeling/gmt/epsilon/interim/

Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.

Code Generation Status

Latest Developments

  • Demonstrator plug-in feature version 0.1.0
    • for Rodin 2.1.x version is available.
  • The Code Generation feature consists of,
    • 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 [[1]]

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_General_Platform_Maintenance&oldid=1381’