Code Generation Activity: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Andy
imported>Andy
Line 4: Line 4:
available from: https://sourceforge.net/projects/codegenerationd/files/
available from: https://sourceforge.net/projects/codegenerationd/files/


The zip file contains a windows XP bundle, v7 bundle, and an update site with install instructions. A simple shared buffer example is provided. This will form the basis of a tutorial (work in progress).
The zip file contains a windows XP bundle, Windows V7 bundle. In addition the update site can be used with install instructions, but 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 (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. 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.
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. 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.

Revision as of 16:44, 29 November 2010

Code Generation Demonstrator

First release: 30 November 2010:

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

The zip file contains a windows XP bundle, Windows V7 bundle. In addition the update site can be used with install instructions, but 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 (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. 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 and by using the update site. The example projects, and the project forming the basis of a simple tutorial are provided in the accompanying zip file.

Mac users - no bundled version available at present, but the update site, install instructions and example projects are available in the advanced directory.

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