D32 Code generation

From Event-B
Revision as of 11:06, 1 December 2010 by imported>Andy (→‎Overview)
Jump to navigationJump to search

Overview

The code generation activity has been undertaken at the University of Southampton led by Michael Butler. Its purpose has been to establish a link between the formal modelling approach of Event-B and code that is suitable for compilation. Development of the approach and the tools to support it involved a number of team members at Southampton, and also at other institutions. The code generation approach draws on our recent experience with technologies such as Shared Event Decomposition [[1]], Event-B EMF, and TextTools. There was collaboration at an early stage with Newcastle University, exploring the commonalities between work-flow and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their Epsilon model-to-model transformation technology.

Motivations

This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.

Choices / Decisions

This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

Available Documentation

This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:

   * Requirements.
   * Pre-studies (states of the art, proposals, discussions).
   * Technical details (specifications).
   * Teaching materials (tutorials).
   * User's guides. 

A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.

Planning

This paragraph shall give a timeline and current status (as of 28 Jan 2011).