Difference between pages "D23 Code Generation" and "D23 Decomposition"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Pascal
 
Line 1: Line 1:
=Overview and Motivation=
+
= Overview =
 +
The Event-B model decomposition is a new feature in the Rodin platform.
  
Code generation is an important part of the formal engineering tool chain that will enable complete support for development from high-level models down to executable implementations. Work has commenced on the development of support for code generation from Event-B models.  This is a new line of work for DEPLOY that was not identified in the original Description of Work for the project.  During the first year of the project, as the Deployment Partners gained experience with deployment of formal modelling, it became clear that having 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 is especially true for Bosch and Space Systems Finland (SSF). During the DEPLOY re-focus at Month 18, it was decided to introduce a code generation task into a revised workplan and devote resources to this task.
+
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>.
  
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. In essence, this involves programs structured as tasks running concurrently such as supported by the Ada tasking model.  The individual tasks are sequential programs and tasks share state variables via some form of monitor mechanism.  For real-time control, both periodic and aperiodic task should be supported; tasks should have priorities to ensure appropriate responsiveness of the control software.
+
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specifications and developments. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible of the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.
  
For the DEPLOY pilots, it is 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 is required. It is not our intention to develop a fully-fledged industrial-strength code generation framework within the lifetime of the DEPLOY project.  Instead an aim is to develop a sufficient framework to act as a proof-of-concept to enable code generation for the Bosch and SSF pilots.  A further aim is to gain practical experience with a prototype code generation framework that will serve as a basis for future R&D on a scalable code generation framework.
+
= Motivations =
The code generation work is being lead by Southampton with initial input from Newcastle.
+
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.
  
=Choices / Decisions=
+
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.
Three candidate approaches have been posited as follows:
+
This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
* Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation.
+
: 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].
* Synthesise sequential and concurrent code from existing low-level Event-B models.
 
* Exploit the code generation facilities of Atelier-B for “classical” B.
 
  
Approach 3 will be important for STS in WP2 as it will enable integration of Rodin with the existing development process in STS with AtelierB and some effort will be devoted to this. However, this approach will not address the needs of all the deployments because of the overhead involved in having to use AtelierB alongside Rodin as well as the lack of support for concurrent code generation in AtelierB. Supporting Approach 2 has the attraction that developers can remain within the uniform language framework of Event-B.  However, it is not clear that we can meet the real-time performance guarantees required for embedded systems with this approach within the lifetime of the DEPLOY project.  
+
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>.
  
While we will pursue some exploration of this approach, we will focus most effort on Approach 1 as this will enable existing techniques for real-time programming to be incorporated in later stages of development.  Language support for explicit sequential and concurrent programs will be defined to enable construction of code-oriented models at low levels of refinement. We refer to this form of Event-B as task-oriented. A code generation framework will be developed to enable automated generation of C and Ada subsets suitable for real-time embedded systems from code-oriented models.  A refinement-based proof method for code-oriented models will be defined and incorporated into the Rodin toolset.
+
The model decomposition leads to some interesting benefits:
 +
* 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.
  
An important requirement is that the code generation framework be amenable to extension and tailoring for specific needs.  Rather than hard-wiring the code generation rules into the tool, we will aim to support a declarative rule-based approach to defining translation from task-oriented Event-B to a target implementation language. The translation should be tailorable by modifying or extending the declarative translation rules.  We will explore the use of a model-based transformation framework such as ATL or ETL for this purpose.  Rather than fixing on a specific set of implementation-level data types, we will exploit the mathematical extension facility being developed for Rodin to enable a flexible approach to defining implementation-level data structures.  For example, arrays could be supported by defining a new theory of arrays.  This theory would define array declarations and operators along with an appropriate set of proof rules for arrays to enable reasoning.  Appropriate declarative rules would then be defined to translate array declarations and expressions to appropriate code in the target language.
+
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 issue.
  
=Tasking Language=
+
= Choices / Decisions =
The Event-B tasking language will support the following sequential and concurrent algorithmic constructs:
+
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).
{| border="1"
 
|Behaviour
 
|Algorithmic Construct
 
|-
 
|Sequence
 
|;
 
|-
 
|Branching
 
|if
 
|-
 
|Iteration
 
|while
 
|-
 
|Task/Thread/Process
 
|task
 
|-
 
|Shared variables
 
|machine
 
|}
 
  
A task-oriented model will be definable using the following abstract syntax
+
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:
{| border="0"
+
* 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).
|Task := 
+
* 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.
| '''task'''  Name 
+
* Recursivity. Thus, it is possible to decompose a previously decomposed model.
|-
 
|
 
| '''variables''' Variables
 
|-
 
|
 
| '''invariants''' Invariants 
 
|-
 
|
 
| '''begin''' TaskBody  '''end'''
 
|}
 
  
{| border="0"
+
Other technical decisions are justified in the specification wiki pages.
| TaskBody := 
 
|-
 
|
 
| Event
 
|-
 
|
 
|  <math>|</math> TaskBody  ;  TaskBody
 
|-
 
|
 
|  <math>|</math> '''if'''    Guard→ TaskBody  []  … []  Guard→ TaskBody  '''fi'''
 
|-
 
|
 
|  <math>|</math> '''do'''  Guard→ TaskBody  []  … []  Guard→ TaskBody  '''od'''
 
|}
 
  
The sequence, branching and iteration constructs correspond to their imperative counterparts. The task construct provides a means to specify the actions of interleaving, concurrent executions. A task may be implemented by an Ada task, or a thread in C. A task, in isolation, is a sequential program with clearly identified atomic steps, and each step corresponding to an atomic event.  
+
= Available Documentation =
 +
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
 +
* Shared variables (A-style) decomposition specification.  
 +
:See [[Event_Model_Decomposition | http://wiki.event-b.org/index.php/Event_Model_Decomposition]].  
 +
* Decomposition plug-in user's guide.
 +
:See [[Decomposition_Plug-in_User_Guide | http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide]].
  
The standard machine construct provides the mechanism for sharing data between the executing tasks. The interaction between a task and a machine can be represented synchronized event composition as currently supported by the synchronised-event plug-in.  The generated implementation will need to ensure that a task has mutually exclusive access to the variables represented in the machine. This is provided by a machine’s atomic events. A machine representing shared variables may be implemented by an Ada protected object, or in C by an explicit Mutex variable and appropriate lock acquisition.
+
= Planning =
 
+
The decomposition plug-in is available since release 1.2 of the platform.
To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority.
+
:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes].
{| border="0"
+
:and [http://wiki.event-b.org/index.php/Decomposition_Release_History http://wiki.event-b.org/index.php/Decomposition_Release_History].
|Task :
 
|-
 
|
 
| '''task'''  Name 
 
|-
 
|
 
| '''tasktype''' '''periodic'''(p) <math>|</math>  '''triggered''' <math>|</math> '''repeating''' <math>|</math> '''oneshot'''
 
|-
 
|
 
| '''priority''' n
 
|-
 
|
 
| ...
 
|}
 
 
 
A tasktype is used to indicate the scheduling requirements for the required activity.  It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is parameterised by a time valueActivity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype. In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.
 
It may be decided that, during a program’s execution, some of the activities should take precedence over some others.  We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.
 
 
 
=Methodological Support=
 
As previously outlined, the atomic steps of a sequential task will be syntactically explicit.  This is in order to facilitate a direct mapping of task steps with events of an abstract machine.  The development approach that we plan to support fits with the general refinement approach of Event-B in that explicit tasking will be introduced as part of a refinement step.  A common approach to specifying a problem is to represent some desired outcome as a single abstract atomic event.  Common patterns of refinement of such abstract events found in existing Event-B developments are as follows:
 
 
 
#Choice refinement:  Event E is refined to E1 [] E2 []…[] En, where each Ei refines E
 
#Sequential refinement:  Event E is refined to E1 ; E2 ; … En, where some Ei refines E and the other Ej refine skip.
 
#Loop refinement: Event E is refined to E1 ; do E2 od ; E3, where E3 refines E and E1 and E2 refine skip.
 
 
 
These patterns motivate a simpler subset of the tasking language as follows
 
{| border="0"
 
| TaskBody :
 
|-
 
|
 
| Event
 
|-
 
|
 
|  <math>|</math> TaskBody  ;  TaskBody
 
|-
 
|
 
|  <math>|</math> '''if'''    Event  [] … []  Event  '''fi'''
 
|-
 
|
 
|  <math>|</math> '''do'''  Event  '''endwith'''  Event  '''od'''
 
|}
 
 
 
Initially we will support refinement to this subset by providing special structure-introduction refinement rules in the manner of the refinement calculus.  We will also develop support for a generalisation of this set of rules in which the abstract model consists of a group of atomic events, with each event representing a different possible outcome. An example use of such a group would be to have an event to represent the normal behaviour of some system feature and a separate event to represent the error behaviour of the feature.
 
 
 
The above rules prevent the immediate introduction of nested tasking structures such as nested loops.  Following the approach found in the refinement calculus and common practice in Event-B refinements, such nested structures may be introduced through further refinement steps. For example, to introduce a nested loop, the outer loop is first introduced and the inner loop is introduced in a subsequent refinement step. We  will explore generalising the refinement support for tasks to support nesting through refinement along these lines.
 
 
 
=Timescales=
 
We refer to the tasking language outlined above as Version V1. Our planned timescales for further work on code generation are as follows:
 
*June 2010: demonstrator tool for language V1.
 
*June 2010: initial support for user defined datatypes (mathematical extensions).
 
*From June to October 2010:  experimentation with and assessment of the demonstrator tool on the WP1 and WP3 pilots leading to feedback on V1 and the tool.
 
*Jan 2011:  algorithmic language definition V2.
 
*June 2011: prototype tool for V2.
 
*From June to October 2011:  experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots.
 
  
 
[[Category:D23 Deliverable]]
 
[[Category:D23 Deliverable]]

Revision as of 16:05, 20 November 2009

Overview

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 M into several independent sub-models M_1, ...,M_n.

Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specifications and developments. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible of the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.

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

The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model M into smaller sub-models M_1, ..., M_n. 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 MR in a way that guarantees that MR refines M.

The model decomposition leads to some interesting benefits:

  • 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 issue.

Choices / Decisions

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:

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

Available Documentation

The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:

  • Shared variables (A-style) decomposition specification.
See http://wiki.event-b.org/index.php/Event_Model_Decomposition.
  • Decomposition plug-in user's guide.
See http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide.

Planning

The decomposition plug-in is available since release 1.2 of the platform.

See http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes.
and http://wiki.event-b.org/index.php/Decomposition_Release_History.