D32 Code generation

THIS DOCUMENT IS NOT YET COMPLETE !!!

Overview

The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as Shared Event Decomposition [[1]], and the EMF Framework for Event-B [[2]]. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in [[3]] and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their Epsilon [[4]] model-to-model transformation technology.

Motivations

The decision was taken in 2009 [[5]] to include code generation as a project goal. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.

Choices / Decisions

During the last year we have focussed on supporting the generation of code for typical real-time embedded control software. To this end we have developed a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Individual tasks are treated as sequential programs; these are modelled by an extension to Event-B, called Tasking Machines. Tasks have mutually exclusive access to state variables through the use of protected resources. The protected resources correspond to Event-B machines. For real-time control, periodic and one-shot activation is currently supported; and it is planned to support aperiodic tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software.

For the DEPLOY project, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated. In the past year our goal has been to provide an approach, and tool support, to act as a proof-of-concept. We also gained much practical experience with the development of a code generation framework.

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