Difference between pages "Code Generation Activity" and "Current Developments"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Mathieu
 
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
+
{{TOCright}}
=== Code Generation Feature - Version 0.2.0 For Rodin 2.3===
+
This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations about your own development to keep the community informed''
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.
 
* Tasking Event-B to Event-B translator in fully 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.
 
  
 +
== Deploy Tasks ==
 +
The following tasks were planned at some stage of the [[Deploy]] project.
 +
=== Core Platform ===
 +
==== New Mathematical Language ====
 +
==== Rodin Index Manager ====
 +
[[Systerel]] is in charge of this task.
 +
{{details|Rodin Index Design|Rodin index design}}
  
TODO
+
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.  
* 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 ===
+
==== Undo / Redo ====
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.
+
[[Systerel]] is in charge of this task.
 +
{{details|Undo Redo Design|Undo/Redo design}}
 +
{{TODO|describe current work in [[Undo Redo Design]]}}
  
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
+
{{TODO|add a short summary about current work for undo/redo here}}
  
* 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/
+
==== Text Editor ====
 +
[[Düsseldorf]] has a prototype text-based editor for Event-B (courtesy of Fabian Fritz). As of end of sempteber 2008, it still needs more work to fully integrate into Rodin.
  
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
=== Plug-ins ===
 +
==== Requirement Management Plug-in ====
 +
[[User:Jastram|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin|Requirements Management Plug-in]].
  
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].
+
{{See also|ReqsManagement|Requirements Tutorial|l1=Requirements Management Plug-in}}
  
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].
+
This plug-in allows:
 +
* Requirements to be edited in a set of documents (independently from Rodin)
 +
* Requirements to be viewed within Rodin
 +
* Individual Requirements to be linked to individual Event-B-Entities
 +
* A basic completion test to be performed
  
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
==== UML-B Plug-in ====
 +
[[Southampton]] is in charge of [[UML-B]] plug-in.
  
Released 24 January 2011.
+
* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
  
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
*Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which has formerly been denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
  
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
* Better support for state machine refinement in UML-B. This revision to UML-B allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines.
  
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
==== ProB Plug-in ====
 +
[[Düsseldorf]] is in charge of [[ProB]].
 +
{{details|ProB current developments|ProB current developments}}
  
The code generation tutorial examples are available for download at:
+
===== Work already performed =====
  
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences.
 +
The model checking feature is now also accessible.
 +
It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB.
 +
On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB
 +
specifications from Siemens).
  
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:
+
On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.
  
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
===== Ongoing and future developments=====
  
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
We are currently developing a new, better user interface.
 +
We also plan to support multi-level animation with checking of the gluing invariant.
  
== Code Generation Status ==
+
We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:
=== Latest Developments ===
+
* an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
* Demonstrator plug-in feature version 0.1.0
+
* a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
** for Rodin 2.1.x version is available.
+
* a 2D viewer to inspect the state space of the specification
  
* 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 ===
+
== Exploratory Tasks ==
 +
=== One Single View ===
 +
[[Maria]] is in charge of this exploratory work during is internship.
 +
{{details|Single View Design|Single View Design}}
 +
The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.
  
* 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 ==
+
== Others ==
* 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
 
  
 +
=== AnimB ===
 +
[[Christophe]] devotes some of its spare time for this plug-in.
 +
{{details|AnimB Current Developments|AnimB Current Developments}}
 +
The current developments around the [[AnimB]] plug-in encompass the following topics:
 +
;Live animation update
 +
:where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
 +
;Collecting history
 +
:The history of the animation will be collected.
  
 +
=== Team-Based Development ===
  
 +
; Usage Scenarios
 +
: In order to understand the problem properly, [http://www.stups.uni-duesseldorf.de/ Düsseldorf] created a number of usage [[Scenarios for Team-based Development]].
 +
: A page as also been opened for [[Scenarios for Merging Proofs|merging proofs scenarios]].
 
[[Category:Work in progress]]
 
[[Category:Work in progress]]

Revision as of 13:09, 3 October 2008

This page sum up the known developments that are being done around or for the Rodin Platform. Please contributes informations about your own development to keep the community informed

Deploy Tasks

The following tasks were planned at some stage of the Deploy project.

Core Platform

New Mathematical Language

Rodin Index Manager

Systerel is in charge of this task.

For more details on Rodin index design, see Rodin Index Design.

The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

Undo / Redo

Systerel is in charge of this task.

For more details on Undo/Redo design, see Undo Redo Design.

TODO: describe current work in Undo Redo Design

TODO: add a short summary about current work for undo/redo here

Text Editor

Düsseldorf has a prototype text-based editor for Event-B (courtesy of Fabian Fritz). As of end of sempteber 2008, it still needs more work to fully integrate into Rodin.

Plug-ins

Requirement Management Plug-in

Michael at Düsseldorf is in charge of the Requirements Management Plug-in.

See also: Requirements Management Plug-in and Requirements Tutorial

This plug-in allows:

  • Requirements to be edited in a set of documents (independently from Rodin)
  • Requirements to be viewed within Rodin
  • Individual Requirements to be linked to individual Event-B-Entities
  • A basic completion test to be performed

UML-B Plug-in

Southampton is in charge of UML-B plug-in.

  • Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
  • Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which has formerly been denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
  • Better support for state machine refinement in UML-B. This revision to UML-B allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines.

ProB Plug-in

Düsseldorf is in charge of ProB.

For more details on ProB current developments, see ProB current developments.
Work already performed

We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences. The model checking feature is now also accessible. It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB. On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB specifications from Siemens).

On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.

Ongoing and future developments

We are currently developing a new, better user interface. We also plan to support multi-level animation with checking of the gluing invariant.

We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:

  • an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
  • a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
  • a 2D viewer to inspect the state space of the specification


Exploratory Tasks

One Single View

Maria is in charge of this exploratory work during is internship.

For more details on Single View Design, see Single View Design.

The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.


Others

AnimB

Christophe devotes some of its spare time for this plug-in.

For more details on AnimB Current Developments, see AnimB Current Developments.

The current developments around the AnimB plug-in encompass the following topics:

Live animation update
where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
Collecting history
The history of the animation will be collected.

Team-Based Development

Usage Scenarios
In order to understand the problem properly, Düsseldorf created a number of usage Scenarios for Team-based Development.
A page as also been opened for merging proofs scenarios.