Difference between pages "D23 UML-B" and "D32 Code generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
m
 
imported>Andy
 
Line 1: Line 1:
−
=== Overview ===
+
'''THIS DOCUMENT IS NOT YET COMPLETE !!!'''
−
This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.
 
  
−
A new plug-in feature has been developed to provide animation of UML-B state-machine diagrams. This feature was developed by University of Southampton.
+
== General Overview ==
  
−
The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Duesseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.
+
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.
  
−
=== Motivations ===
+
== Motivations ==
  
−
====UML-B improvements====
+
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.
−
The current version of the UML-B tool has been improved to support the refinement of  state-machines. At the last deliverable, refinement of classes was supported and state-machine refinement was beginning to be investigated. The investigation has experimented several notation and methodological alternatives. The design has now been finalised and an implementation has been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of ''transition elaboration'' has been invented to represent this relationship.
 
  
−
Many other minor improvements have been made to the UML-B tool including:
+
== Choices / Decisions ==
−
collapsing empty compartments on diagrams,
+
=== Strategic Overview ===
−
improved navigation between diagrams,
+
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.  
−
improved properties views,
 
−
ability to order classes and class-types in the translation,
 
−
support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems).
 
  
−
====UML-B State-machine Animation====
+
Our main goal this year has been to devise an approach for, and provide tool support for, code generation (initially to Ada). 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.
−
This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.
 
  
−
====EMF Framework for Event-B====
+
=== The Tasking Extension for Event-B ===
  
−
An EMF (Eclipse Modelling Framework) based representation of Event-B was developed and made available as a plug-in feature for Rodin. This enables Event-B machines and contexts to be loaded into EMF based tools. Serialisation (i.e. loading and saving) is performed via the Rodin API. This feature can be viewed as an ''enabling technology''. Hence motivation derives from several sources including:
+
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.
−
* A Text editor was requested by several industrial and academic partners - A fully-featured EMF based text editor ('''Camille''') has been developed by Duesseldorf and is now available.
 
−
* Team-working facilities are required by all industrial partners (particularly Bosch and SSF) - EMF Compare/merge tools are now under investigation to support a '''teamworking''' repository plug-in feature.
 
−
* '''UML-B integration''' - since UML-B is based on EMF, the development of an EMF representation of Event-B enables UML-B concepts to be added as extensions.
 
  
−
=== Choices / Decisions ===
+
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.
  
−
====UML-B improvements====
+
A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). 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.
  
−
The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of ''elaboration'' was introduced, whereby an elaborating  transition contributes guards and actions to the event produced from the elaborated parent transition. Transitions splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to ''bundle'' the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.
+
<center>
 +
{| border="1"
 +
|Construct
 +
|Options
 +
|-
 +
|Machine Type
 +
|DeclaredTask, AutoTask, SharedMachine
 +
|-
 +
|Control
 +
|Sequence, Loop, Branch, EventSynch
 +
|-
 +
|Task Type
 +
|Periodic(n), Triggered, Repeating, OneShot
 +
|-
 +
|Priority
 +
| -
 +
|-
 +
|Event Type
 +
|Branch, Loop, ProcedureDef, ProcedureSynch
 +
|-
 +
|Parameter Type
 +
|ActualIn, ActualOut, FormalIn, FormalOut
 +
|}
 +
</center>
  
−
====UML-B State-machine Animation====
+
The machines in the Tasking Development are extended with the constructs shown in the table, and may be viewed as keywords in a textual representation of the language. With extensions added, a Tasking Development can be translated to a common language model for mapping to implementation source code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of the Event-B project.
−
Initially, we attempted to model the animation state information as an extension to the UML-B meta-model. We discovered technological difficulties in extending EMF models in this way. Therefore, we adopted an alternative solution using an independent meta-model of animation diagrams. These replicate parts of the structure of UML-B but add meta-properties to model the animation. When a model is to be animated, an animation model is constructed programmatically to match the UML-B model. Thereafter, the animation runs independently of UML-B. This has the additional benefit that the diagram can be simplified and tailored to better suit animation. For example, removing the editing palette.
 
  
−
====EMF Framework for Event-B====
+
=== Tasking Machines ===
−
The structure of the EMF meta-model for Event-B was studied in great detail. Various options for  sub-packaging the model were tried but it has been found that it is more convenient for users to keep a simple package structure. Currently this consists of three packages; a ''core'' package containing abstract basis and project level meta-model, a ''machine'' package and a ''context'' package. A flexible abstract basis has been derived through experimentation. The abstract basis consists of an inheritance hierarchy of abstract meta-classes which provide great flexibility for writing code that deals with the meta-model in as generic a manner as possible. A driving factor in the design was to support both project level tools and component level tools. The latter should be able to manipulate a single machine or context without loading referenced components. This was achieved customising the EMF proxies (used in references) so that they are calculated lazily (when a request to resolve is received).
+
The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines are related to the concept of an Ada task. These can be implemented in Ada using tasks, in C using the pthread library C, or in Java using threads.
  
−
=== Available Documentation ===
+
* Tasking Machines may be characterised by the following types:
 +
** AutoTasks - Singleton Tasks.
 +
** Declared tasks - (Not currently used) A task template relating to an Ada ''tasktype'' declaration.
 +
** TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
 +
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
  
−
UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:- http://eprints.ecs.soton.ac.uk/18268/
+
=== Shared Machines ===
 +
A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.
  
−
A tutorial on how to refine state-machines is available on the wiki: [[Refinement_of_Statemachines]]
+
* Applied to the Shared Machine we have:
 +
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
  
 +
=== Tasks and Events ===
 +
==== Control Constructs ====
 +
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.
  
−
State-machine animation is described on the wiki here:- [[UML-B_-_Statemachine_Animation]]
+
* We have the following constructs available in the Tasking Machine body:
 +
** Sequence - for imposing an order on events.
 +
** Branch - choice between a number of mutually exclusive events.
 +
** Loop - event repetition while it's guard remains true.
 +
** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do no share state.  The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
 +
** Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.
  
−
It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18261/
+
==== Implementing Events ====
 +
An event's role in the implementation is identified using the following extensions which are added to the event. Events used in task bodies are 'references' that make use of existing event definitions from the abstract development. The events are extended. to assist with translation, with a keyword indicating their role in the implementation.
  
 +
* Event implementation.
 +
** Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.
 +
** Loop - The task's event guard maps to the loop condition and actions to to loop body. If the loop refers to a Shared Machine event then it is mapped to a simple procedure call.
 +
** ProcedureSych - This usually indicates to the translator that the event maps to a subroutine, but an event in a task may not require a subroutine implementation if its role is simply to provide parameters for a procedure call.
 +
** ProcedureDef - Identifies an event that maps to a (potentially blocking) subroutine definition. Event guards are implemented as a conditional wait; in Ada this is an entry barrier, and in C may use a pthread condition variable .
  
−
The EMF Framework for Event-B is described on the wiki here:- [[EMF_framework_for_Event-B]]
+
In an implementation, when an subroutine is defined, its formal parameters are replaced by actual parameter values at run-time. To assist the code generator we extend the Event-B parameters. We identify formal and actual parameters in the implementation, and add the following keywords to the event parameters, as follows:
  
−
It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18262/
+
* Event parameter types
 +
** FormalIn FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
 +
** ActualIn, ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.
  
−
=== Planning ===
+
=== Other Technical Issues ===
 +
==== Translation Technology ====
 +
In order to provide a structured extensible code generation tool it was decided to use a multi-stage translation approach. The Event-B EMF model provided by the Event-B EMF Framework is extended to accommodate the tasking constructs as described above. The Tasking model is then translated to an intermediate model, the Common Language Model. The Common Language Meta-model is an abstraction of some useful generic programming constructs such as sequence, loop, branch and subroutine call/definition and so on. The translation of the Common Language Model to programme source code is then a relatively small step. The main translation activity takes place in the step between Tasking and Common Language models.
  
−
UML-B integration
+
The decision was made to use Epsilon <ref name = "Epsilon"> </ref> to facilitate model to model translation for this stage. It was felt that an extensible, easily maintainable solution was required for this. Various model-to-model technologies (Java code, ATL, Epsilon) were appraised and it was judged that the Epsilon tool best matched our requirements. It proved to be a good choice initially for the specification of translations, especially in simpler areas of the project where the correspondence between models were simple. However the lack of debugging facilities, and productivity enhancements that are found in more mature tools, somewhat hindered rapid development as the project increased in complexity.
−
* Develop extensibility mechanisms for EMF Event-B framework via experimentation with structured data (Records) plug-in.
 
−
* Re-engineer UML-B Context diagrams as a diagrammatic view of Records
 
  
−
* Re-engineer UML-B package diagram based on EMF Event-B framework.
+
==== Implementation - Source Code ====
 +
Early in the current phase of work we identified the possibility of translating the Common Language Model to EMF models of programming languages such as Ada and C, in addition to producing textual source. While the EMF route still remains an option, it was decided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ada editor, and was by far the optimal route for this phase of the code generation activity in DEPLOY.
 +
 
 +
==== Editing the Tasking Model ====
 +
The editor for the Tasking Development is based on a EMF tree-editor. The tree editor provides a facility for adding the extensions to Event-B constructs. The readability of the editor is enhanced by a PrettyPrinter, which provides a textual version of the Tasking Development, which is easier to read. It is envisaged that the textual notation will be fully integrated as a Camille extension when the facility/resources become available.
 +
 
 +
=== The Tool 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 ==
 +
=== Technical Background ===
 +
 
 +
Much insight was gained during the work on code generation reported in the thesis ''Providing Concurrent Implementations for Event-B Developments'' <ref name="aeThesis">http://eprints.ecs.soton.ac.uk/20826/</ref>
 +
 
 +
Tooling issues were reported in a paper ''Tool Support for Event-B Code Generation''
 +
<ref name = "toolSupport">http://eprints.ecs.soton.ac.uk/20824/</ref>
 +
which was presented at ''Workshop on Tool Building in Formal Methods'',
 +
http://abzconference.org/
 +
 
 +
There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.
 +
 
 +
=== For users ===
 +
 
 +
There is a wiki page at http://wiki.event-b.org/index.php/Code_Generation_Activity
 +
 
 +
There is a tutorial at http://wiki.event-b.org/index.php/Code_Generation_Tutorial
 +
 
 +
== Planning ==
 +
 
 +
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
 +
 
 +
== References ==
 +
 
 +
<references/>
 +
 
 +
[[Category:D32 Deliverable]]

Revision as of 13:19, 3 December 2010

THIS DOCUMENT IS NOT YET COMPLETE !!!

General 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 to include code generation as a project goal [5]. 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

Strategic Overview

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 (initially to Ada). 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[6] 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 programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). 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.

Construct Options
Machine Type DeclaredTask, AutoTask, SharedMachine
Control Sequence, Loop, Branch, EventSynch
Task Type Periodic(n), Triggered, Repeating, OneShot
Priority -
Event Type Branch, Loop, ProcedureDef, ProcedureSynch
Parameter Type ActualIn, ActualOut, FormalIn, FormalOut

The machines in the Tasking Development are extended with the constructs shown in the table, and may be viewed as keywords in a textual representation of the language. With extensions added, a Tasking Development can be translated to a common language model for mapping to implementation source code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of the Event-B project.

Tasking Machines

The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines are related to the concept of an Ada task. These can be implemented in Ada using tasks, in C using the pthread library C, or in Java using threads.

  • Tasking Machines may be characterised by the following types:
    • AutoTasks - Singleton Tasks.
    • Declared tasks - (Not currently used) A task template relating to an Ada tasktype declaration.
    • TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
    • Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.

Shared Machines

A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.

  • Applied to the Shared Machine we have:
    • A SharedMachine keyword that identifies a machine as a Shared Machine.

Tasks and Events

Control Constructs

Each Tasking Machine has a task body which contains the flow control, or algorithmic, constructs.

  • We have the following constructs available in the Tasking Machine body:
    • Sequence - for imposing an order on events.
    • Branch - choice between a number of mutually exclusive events.
    • Loop - event repetition while it's guard remains true.
    • Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do no share state. The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
    • Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.

Implementing Events

An event's role in the implementation is identified using the following extensions which are added to the event. Events used in task bodies are 'references' that make use of existing event definitions from the abstract development. The events are extended. to assist with translation, with a keyword indicating their role in the implementation.

  • Event implementation.
    • Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.
    • Loop - The task's event guard maps to the loop condition and actions to to loop body. If the loop refers to a Shared Machine event then it is mapped to a simple procedure call.
    • ProcedureSych - This usually indicates to the translator that the event maps to a subroutine, but an event in a task may not require a subroutine implementation if its role is simply to provide parameters for a procedure call.
    • ProcedureDef - Identifies an event that maps to a (potentially blocking) subroutine definition. Event guards are implemented as a conditional wait; in Ada this is an entry barrier, and in C may use a pthread condition variable .

In an implementation, when an subroutine is defined, its formal parameters are replaced by actual parameter values at run-time. To assist the code generator we extend the Event-B parameters. We identify formal and actual parameters in the implementation, and add the following keywords to the event parameters, as follows:

  • Event parameter types
    • FormalIn FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
    • ActualIn, ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.

Other Technical Issues

Translation Technology

In order to provide a structured extensible code generation tool it was decided to use a multi-stage translation approach. The Event-B EMF model provided by the Event-B EMF Framework is extended to accommodate the tasking constructs as described above. The Tasking model is then translated to an intermediate model, the Common Language Model. The Common Language Meta-model is an abstraction of some useful generic programming constructs such as sequence, loop, branch and subroutine call/definition and so on. The translation of the Common Language Model to programme source code is then a relatively small step. The main translation activity takes place in the step between Tasking and Common Language models.

The decision was made to use Epsilon [4] to facilitate model to model translation for this stage. It was felt that an extensible, easily maintainable solution was required for this. Various model-to-model technologies (Java code, ATL, Epsilon) were appraised and it was judged that the Epsilon tool best matched our requirements. It proved to be a good choice initially for the specification of translations, especially in simpler areas of the project where the correspondence between models were simple. However the lack of debugging facilities, and productivity enhancements that are found in more mature tools, somewhat hindered rapid development as the project increased in complexity.

Implementation - Source Code

Early in the current phase of work we identified the possibility of translating the Common Language Model to EMF models of programming languages such as Ada and C, in addition to producing textual source. While the EMF route still remains an option, it was decided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ada editor, and was by far the optimal route for this phase of the code generation activity in DEPLOY.

Editing the Tasking Model

The editor for the Tasking Development is based on a EMF tree-editor. The tree editor provides a facility for adding the extensions to Event-B constructs. The readability of the editor is enhanced by a PrettyPrinter, which provides a textual version of the Tasking Development, which is easier to read. It is envisaged that the textual notation will be fully integrated as a Camille extension when the facility/resources become available.

The Tool 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

Technical Background

Much insight was gained during the work on code generation reported in the thesis Providing Concurrent Implementations for Event-B Developments [7]

Tooling issues were reported in a paper Tool Support for Event-B Code Generation [8] which was presented at Workshop on Tool Building in Formal Methods, http://abzconference.org/

There are technical notes available [9], that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.

For users

There is a wiki page at http://wiki.event-b.org/index.php/Code_Generation_Activity

There is a tutorial at http://wiki.event-b.org/index.php/Code_Generation_Tutorial

Planning

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

References

  1. ↑ http://wiki.event-b.org/index.php/Event_Model_Decomposition
  2. ↑ http://wiki.event-b.org/index.php/EMF_framework_for_Event-B
  3. ↑ http://wiki.event-b.org/index.php/Flows
  4. ↑ 4.0 4.1 http://www.eclipse.org/gmt/epsilon/ Cite error: Invalid <ref> tag; name "Epsilon" defined multiple times with different content
  5. ↑ http://wiki.event-b.org/index.php/D23_Code_Generation
  6. ↑ http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d108734/Andy%20Edmunds%20-%20Code%20Generation%20Slides.pdf
  7. ↑ http://eprints.ecs.soton.ac.uk/20826/
  8. ↑ http://eprints.ecs.soton.ac.uk/20824/
  9. ↑ http://wiki.event-b.org/images/Translation.pdf
Retrieved from ‘https://wiki.event-b.org/index.php?title=D23_UML-B&oldid=2327’