Code Generation Activity

From Event-B
Revision as of 16:33, 29 November 2010 by imported>Andy (→‎Development Repository)
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Demonstrator Version Release

Date: 30 November 2010:

available from: https://sourceforge.net/projects/codegenerationd/files/

The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code-Gen plug-ins together with a patch plug-in. The patch plug-in is required to correct a difficulty that we encountered with the org.eventb.emf.persistence plug-in. Simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed so no further configuration should be necessary.

A non-bundled version can be created using the info in the advanced folder using the update site. An example project, and a project forming the basis of a simple tutorial are provided in the accompanying zip file. The content in the zip file is already included in the bundled version.

Mac users - sorry no bundled version available at present, but the update site, install instructions and example projects are available in the advanced directory. We could create a bundled version upon request; meanwhile we are be working on a Rodin 2.0 version, which should be available through the usual update mechanism.

A Step by Step tutorial will be available soon

The SVN repository for code generation resides here:

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration

The SVN repository for tagged builds is here:

svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/tags/CodeGeneration

Completed/Ongoing Work

  • Demonstration plug-in,
    • ready for deployment.
    • deployment/Integration Testing under way.
  • The plug-in 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.
    • 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 Demonstration Plug-in Release

The demonstration plug-in is planned for release around November-end 2010, if all goes well. It must be emphasised that the Code Generation (CG) Feature 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. We will be working on this aspect in due course.

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