Difference between revisions of "Code Generation Activity"

From Event-B
Jump to navigationJump to search
imported>Andy
imported>Andy
Line 20: Line 20:
 
Select 'the Epsilon Core (Incubation)' component.
 
Select 'the Epsilon Core (Incubation)' component.
  
=== 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
 
  
 
== Code Generation Status ==
 
== Code Generation Status ==

Revision as of 11:54, 25 January 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

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 (pending).

The code generation tutorial examples are available at:

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

A prerequisite; install Epsilon manually. The automatic install utility does not seem to work for this feature. The Epsilon update site is available at:

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

Select 'the Epsilon Core (Incubation)' component.


Code Generation Status

Current Work

  • Demonstrator plug-in,
    • Rodin 1.3.1 version is ready for release.
  • 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.

Ongoing Work

  • A tutorial
    • Step 1 - Create the tasking development.
    • Step 2 - Add annotations.
    • Step 3 - Invoke translators.

Future Work

  • For the next release, our target is
    • Rodin 2.0 compatibility.
    • Introduction of sensed variables.
    • Support for Interrupts.
    • Event grouping in shared machines mapping to branching statements in protected objects.
    • 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