Difference between pages "D32 Code generation" and "CamilleX"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
 
Line 1: Line 1:
'''THIS DOCUMENT IS NOT YET COMPLETE !!!'''
+
{{TOCright}}
 +
Return to [[Rodin Plug-ins]]
  
== General Overview ==
+
The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
 +
Extension to Event-B including the ''machine inclusion'' mechanism is also supported.
  
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'' <ref name = "SharedEventDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">http://wiki.event-b.org/index.php/EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">http://wiki.event-b.org/index.php/Flows </ref> and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.
+
<br style="clear: both" />
  
== Motivations ==
+
Please have a look also at the [[CamilleX User Guide]].
  
The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> http://wiki.event-b.org/index.php/D23_Code_Generation </ref>. 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.
+
=== Current version ===
 +
The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the ''CamilleX'' category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.
  
== Choices / Decisions ==
+
=== Principles ===
=== Strategic Overview ===
+
The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.
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 evolved a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Individual tasks are treated as sequential programs; these tasks 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.
 
 
 
Our main goal this year has been to devise an approach for, and provide tool support for, code generation. In accord with the resources available during the year it was decided to limit the provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will allow interested parties to explore the approach.
 
 
 
=== The Tasking Extension for Event-B ===
 
 
 
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d108734/Andy%20Edmunds%20-%20Code%20Generation%20Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
 
 
 
Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a tasking development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Events For Tasking]]) to facilitate code generation.
 
 
 
 
 
A tasking development is generated automatically, as directed by the user. The tasking development consists of a number of machines, and contexts where they are seen. In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.
 
 
 
<center>
 
{| border="1"
 
|Construct
 
|Options
 
|-
 
|Machine Type
 
|Declared Task, AutoTask, Shared Machine
 
|-
 
|Control
 
|Sequence, Loop, Branch, EventSynch
 
|-
 
|Task Type
 
|Periodic(n), Sporadic, Repeating, One-shot
 
|-
 
|Priority
 
| -
 
|-
 
|Event Type
 
|Branch, Loop, ProcedureDef, ProcedureSynch
 
|-
 
|Parameter Type
 
|ActualIn, ActualOut, FormalIn, FormalOut
 
|}
 
</center>
 
 
 
The constructs shown in the table provide the information that is necessary to generate an implementation.
 
 
 
=== Tasking - Algorithmic Constructs ===
 
 
 
* Tasking constructs:
 
** Sequence, Branch, Loop.
 
** Event-wrappers.
 
** Event Synchronisation.
 
 
 
=== Events For Tasking ===
 
Event implementation. Branch, Loop, ProcedureSych, ProcedureDef
 
 
 
Event parameter types. FormalIn FormalOut, ActualIn, ActualOut
 
 
 
=== Tasking Machines ===
 
Auto-Tasks.
 
 
 
Declared tasks.
 
 
 
Task type.
 
 
 
Task priority.
 
 
 
=== Shared Machines ===
 
 
 
Events can only be ProcedureDef or ProcedureSynch
 
 
 
Parameters of ProcedureSynch can only be FormalIn or FormalOut
 
 
 
ProcedureDef - parameters not allowed.
 
 
 
 
 
=== Other Technical Issues ===
 
 
 
Meta-models: The use of Epsilon for translation.
 
 
 
=== The Deliverable ===
 
The demonstrator tool was released on 30 November 2010, and is available as an update site, or bundled Rodin package from:
 
https://sourceforge.net/projects/codegenerationd/files  
 
 
 
Sources are available from:
 
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
 
 
 
The tool is based on a build of Rodin 1.3.1 (not Rodin 2.0.0 due to dependency conflicts).
 
 
 
* The Code Generation tool 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 (IL1).
 
** 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.
 
 
 
== Available Documentation ==
 
 
 
pre study
 
http://eprints.ecs.soton.ac.uk/20826/
 
 
 
paper
 
http://eprints.ecs.soton.ac.uk/20824/
 
 
 
wiki page
 
http://wiki.event-b.org/index.php/Code_Generation_Activity
 
 
 
tutorial
 
http://wiki.event-b.org/index.php/Code_Generation_Tutorial
 
 
 
technical notes
 
http://wiki.event-b.org/images/Translation.pdf
 
 
 
 
 
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).
 
 
 
== References ==
 
 
 
<references/>
 

Latest revision as of 13:09, 19 July 2021

Return to Rodin Plug-ins

The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines. Extension to Event-B including the machine inclusion mechanism is also supported.


Please have a look also at the CamilleX User Guide.

Current version

The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the CamilleX category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.

Principles

The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.