Difference between pages "D23 Decomposition" and "D32 Code generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Andy
 
Line 1: Line 1:
−
= Overview =
+
'''THIS DOCUMENT IS NOT YET COMPLETE !!!'''
−
The Event-B model decomposition is a new feature in the Rodin platform.
 
  
−
Two methods have been identified in the DEPLOY project for model decomposition: the ''shared variable'' decomposition (or A-style decomposition, after Abrial), and the ''shared event'' decomposition (or B-style decomposition, after Butler). They both answer to the same requirement, namely the possibility to decompose a model <math>M</math> into several independent sub-models <math>M_1, ...,M_n</math>.
+
== General Overview ==
  
−
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specifications and developments. Systerel was more especially responsible of the A-style decomposition. The University of Southampton was in charge of the B-style decomposition.  
+
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 ==
−
One of the most important feature of the Event-B approach is the possibility to introduce new events and data-refinement of variables during refinement steps.
 
  
−
It however results in an increasing complexity of the refinement process when having to deal with many events, many state variables, and consequently many proof obligations.
+
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.
−
This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
 
−
: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf].
 
  
−
The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. The sub-models can then be refined separately and more comfortably than the whole. The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>.
+
== 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.  
  
−
The model decomposition leads to some interesting benefits:
+
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.
−
* Design/architectural decision. It applies in particular when it is noticed that it is not necessary to consider the whole model for a given refinement step, because only a few events and variables are involved instead.
 
−
* Complexity management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
 
−
* Team development. More precisely, it gives a way for several developers to share the parts of a decomposed model, and to work independently and possibly in parallel on them.
 
  
−
Note that the possibility of team development is among the current priorities for all industrial partners. The model decomposition is a first answer to this problematic issue.
+
=== The Tasking Extension for Event-B ===
  
−
= Choices / Decisions =
+
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.
−
The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' vs. ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model (eg. the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems).
 
  
−
Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
+
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.
−
* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (according to the DEPLOY description of work, the decomposition support was expected by the end of 2009).
 
−
* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).
 
−
* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (eg. the static checker, the proof obligation generator and the editor have been extended).
 
−
* Performance.
 
−
* Recursivity. Thus, it is possible to decompose a previously decomposed model.
 
  
−
Other technical decisions are justified in the specification wiki pages.
+
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.
  
−
= Available Documentation =
+
<center>
−
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
+
{| border="1"
−
* Shared variables (A-style) decomposition specification.
+
|Construct
−
:See [[Event_Model_Decomposition | http://wiki.event-b.org/index.php/Event_Model_Decomposition]].
+
|Options
−
* Decomposition plug-in user's guide.
+
|-
−
:See [[Decomposition_Plug-in_User's_Guide | http://wiki.event-b.org/index.php/Decomposition_Plug-in_User's_Guide]].
+
|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>
  
−
= Planning =
+
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.
−
The decomposition plug-in is available since release 1.2 of the platform.
+
 
−
:See [[Rodin_Platform_1.2_Release_Notes | http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes]].
+
=== Tasking Machines ===
 +
The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines map to the concept of a process/thread/task. These can be implemented by Ada tasks, use of the pthread library in C, or Java 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 ===
 +
Shared Machines map to the concept of a protected resource, or monitor. They may be implemented in Ada as a protected object, in C using a mutex lock, or Java monitor.
 +
 
 +
* Applied to the Shared Machine we have:
 +
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
 +
 
 +
=== More Details ===
 +
==== 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.
 +
** Event-wrappers - The 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 this purpose). 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.
 +
 
 +
==== Events In Tasking Developments ====
 +
Event implementation. Branch, Loop, ProcedureSych, ProcedureDef
 +
 
 +
Event parameter types. FormalIn FormalOut, ActualIn, ActualOut
 +
 
 +
* In Shared Machines:
 +
** events can only be designated as ProcedureDef or ProcedureSynch.
 +
** parameters of ProcedureSynch can only be FormalIn or FormalOut
 +
 
 +
* In procedureDef
 +
** parameters are 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 ==
 +
 
 +
 
 +
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/>

Revision as of 13:37, 2 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. 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 map to the concept of a process/thread/task. These can be implemented by Ada tasks, use of the pthread library in C, or Java 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

Shared Machines map to the concept of a protected resource, or monitor. They may be implemented in Ada as a protected object, in C using a mutex lock, or Java monitor.

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

More Details

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.
    • Event-wrappers - The 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 this purpose). 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.

Events In Tasking Developments

Event implementation. Branch, Loop, ProcedureSych, ProcedureDef

Event parameter types. FormalIn FormalOut, ActualIn, ActualOut

  • In Shared Machines:
    • events can only be designated as ProcedureDef or ProcedureSynch.
    • parameters of ProcedureSynch can only be FormalIn or FormalOut
  • In procedureDef
    • parameters are 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

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. ↑ http://www.eclipse.org/gmt/epsilon/
  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_Decomposition&oldid=2293’