Code Generation Activity

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]]