Difference between pages "Code Generation Tutorial" and "D32 Code generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Andy
 
Line 1: Line 1:
−
'''This Page is Under Construction'''
+
=== Overview ===
  
−
=== Tutorial 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. 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'' [[http://wiki.event-b.org/index.php/Event_Model_Decomposition]], and the ''EMF Framework for Event-B'' [[http://wiki.event-b.org/index.php/EMF_framework_for_Event-B]]. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their work on work-flow [[http://wiki.event-b.org/index.php/Flows]] and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' [[http://www.eclipse.org/gmt/epsilon/]] model-to-model transformation technology.
  
−
The aim of the tutorial is to allow users to explore the approach with a relatively simple example. The example uses a shared buffer with reader and writer processes. The tutorial is presented in three stages, making use of the example projects from the download site. There are two translations performed, one is to a common language model (IL1). The second is to an Event-B project which includes a model of the implementation. There is a PrettyPrinter for Ada source code, which uses the common language model.
+
=== Motivations ===
  
−
A typical Event-B development may be refined to the point where it is ready for implementation, but the Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines that are to be implemented (and their seen Contexts) are selected and added to a ''Tasking Development''; the Tasking Development files have the file extension ''.tasking''. The machines in the Tasking Development are then extended with implementation details.
+
The decision was taken in 2009 [[http://wiki.event-b.org/index.php/D23_Code_Generation]] to include code generation as a project goal, and to focus our efforts on supporting the generation of code for typical real-time embedded control software. To this end we have developed a multi-tasking approach such as that supported by 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.
  
−
The example/tutorial projects are,
+
For the DEPLOY pilots, 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.
  
−
{| border="1"
 
−
|SharedBuffer20100819Demo
 
−
|An example project with a completed Tasking Development and IL1 model (post IL1 translation, but before Event-B translation).
 
−
|-
 
−
|Sharedbuffer20100819Tasking
 
−
|Same as the example project above, but with Event-B model translations. The difference being that this development includes a model of the implementation. These are refinements that include a program counter to describe flow of execution in each task.
 
−
|-
 
−
|SharedBuffer20100819Tutorial
 
−
|A bare project for step 1 of the tutorial.
 
−
|-
 
−
|Sharedbuffer20100819Tutorial2
 
−
|A partially completed tasking development for steps 2 and 3 of the tutorial.
 
−
|}
 
  
−
== Preliminaries ==
 
−
Before further discussion of the modelling aspects, we take a look at the PrettyPrint viewers. The PrettyPrinters make the viewing of tasking models easier, and provides a quick route to source code generation. The source code can easily be pasted into an Ada source file from the IL1 Pretty Printer window.
 
−
==== The PrettyPrint View of a Tasking Development ====
 
−
From the top-menu select ''Window/Show View/Other/Tasking Pretty Printer''.
 
  
−
Note that the Tasking PrettyPrinter may have to be closed when editing the Tasking Development, since it can give rise to exceptions. The PrettyPrinter would need further work to make it robust, however it is intended only as a short-term solution.
+
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.
  
−
Open the ''SharedBuffer20100819Demo'' Project and switch to the Resource Perspective. Open the ''.tasking'' model and inspect it. Clicking on the Main, Machine or Event nodes updates the pretty print window.
+
=== Choices / Decisions ===
  
−
==== Viewing Source Code ====
+
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.
  
−
aka. The PrettyPrint View of an IL1 Model.
+
=== Available Documentation ===
  
−
From the top-menu select ''Window/Show View/Other/IL1 Pretty Printer''.
+
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:
  
−
Open the ''SharedBuffer20100819Demo'' Project and switch to the Resource Perspective. Open the ''.il1'' model and inspect it. Clicking on the Protected, Main Entry, or Task nodes updates the pretty print window.
+
    * Requirements.
 +
    * Pre-studies (states of the art, proposals, discussions).
 +
    * Technical details (specifications).
 +
    * Teaching materials (tutorials).
 +
    * User's guides.  
  
−
==== Cleaning the Tasking Development ====
+
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.
  
−
If the ''.tasking'' file has errors, then it may need cleaning. To do this right-click on the ''Main'' node, select ''Epsilon Translation/CleanUp''.
+
=== Planning ===
  
−
== The Tutorial ==
+
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
−
The steps will be as follows,
 
−
* Step 1 - Create the tasking development.
 
−
* Step 2 - Add annotations.
 
−
* Step 3 - Invoke translators.
 
−
 
 
−
==== Creating The Tasking Development ====
 
−
 
 
−
From the Event-B Perspective,
 
−
 
 
−
Open the SharedBuffer20100819Tutorial Project.
 
−
 
 
−
Select the following Machines: Reader, Writer and Shared.
 
−
 
 
−
Right-click and select Make Tasking Development/Generate Tasking Development.
 
−
 
 
−
The new Tasking Development will not be visible in the Event-B perspective, change to the resource perspective, open and inspect the new .tasking file. The Tasking Development contains the machines that we wish to provide implementations for. In order to introduce the new concepts we have prepared a partially complete development.
 
−
 
 
−
Go to the Project SharedBuffer20100819Tutorial2 to begin the next step.
 
−
 
 
−
==== Providing the Annotations for Implementations ====
 

Revision as of 11:48, 1 December 2010

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. 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]], 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 work on work-flow [[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, and to focus our efforts on supporting the generation of code for typical real-time embedded control software. To this end we have developed a multi-tasking approach such as that supported by 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 pilots, 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.


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

Retrieved from ‘https://wiki.event-b.org/index.php?title=Code_Generation_Tutorial&oldid=2188’