Difference between pages "D23 Code Generation" and "D23 Flow Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>WikiSysop
 
imported>Alexili
 
Line 1: Line 1:
=Overview and Motivation=
+
= Overview =
  
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.
+
Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows plugin addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.
  
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.
+
Sequential composition of events may be expressed in a number of ways:
 +
* event immediately follows another event; no other events may take place between the composed events.
 +
* event eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.
 +
* event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.
  
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.
+
Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives.  
The code generation work is being lead by Southampton with initial input from Newcastle.
 
  
=Choices/Decisions=
+
= Motivations =
Three candidate approaches have been posited as follows;
 
• Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation
 
• 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.  
+
There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:
 +
* for some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model;
 +
* explicit control flow may help in proving properties related to event ordering;
 +
* sequential code generation requires some form of control flow information;
 +
* since event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information;
 +
* a potential for a visual presentation based on control flow information;
 +
* bridging the gap between high-level workflow and architectural languages, and Event-B.
  
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.
+
It is also hoped that the plugin would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.  
  
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.
+
= Choices / Decisions =
  
=Tasking Language=
+
The primary functionality of the plugin is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plugin and the proof obligations related to flow appear in the list of the model proof obligations.
The Event-B tasking language will support the following sequential and concurrent algorithmic constructs:
 
{| 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
+
One of the lessons learned with an initial plugin prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are not familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF: an Eclipse library for manipulating EMF models using graphical editors.
{| border="0"
 
|Task :
 
|-
 
|
 
| task  Name 
 
|-
 
|
 
| variables Variables
 
|-
 
|
 
| invariants Invariants 
 
|-
 
|
 
| begin TaskBody  end
 
|}
 
  
{| border="0"
+
= Available Documentation =
| 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.  
+
There is a [[Flows|wiki]] page summarising proof obligation involved in proving machine/flow consistency.
  
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 plugin.  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 plugin is to be available for the time of release of Platform version 1.2.
  
To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority
+
[[Category:D23 Deliverable]]
{| border="0"
 
|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 value.  Activity 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 (math extn)
 
*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
 

Revision as of 12:54, 30 November 2009

Overview

Event-B, being an event systems formalism does not have a mechanism for explicitly defining event ordering. Although event guards may express any desired event ordering, the ability to have a summary of possible event flows in a concise and compact form is useful for many tasks, for example, code generation and connecting with other formalisms. The flows plugin addresses one aspect of event ordering: it allows a modeller to specify and prove that a given sequence of events does not contradict a given machine specification. More precisely, if we were to execute a machine step-by-step following our prescribed sequence of events we would not discover divergencies and deadlocks not already present in the original machine. In other words, the constraining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desired model properties proved before are preserved.

Sequential composition of events may be expressed in a number of ways:

  • event immediately follows another event; no other events may take place between the composed events.
  • event eventually follows an event; thus, although there is an interference from other events, it is guaranteed that the second is eventually enabled.
  • event may follow an event; this is the weakest form of connection when we only say that it may be the case that the second event follows the first event; it may happen, however, that some other event interferes and the second event is delayed or is even not enabled ever.

Although the last case may seem the least appealing, it is the one that forms the basis of the Flows plugin. The primary reason for offering such a weak guarantee is proof effort required for stronger types of connectives.

Motivations

There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:

  • for some problems the information about event ordering is an essential part of requirements; it comes as a natural expectation to be able to adequately reproduce these in a model;
  • explicit control flow may help in proving properties related to event ordering;
  • sequential code generation requires some form of control flow information;
  • since event ordering could restrict the non-determinism in event selection, model checking is likely to be more efficient for a composition of a machine with event ordering information;
  • a potential for a visual presentation based on control flow information;
  • bridging the gap between high-level workflow and architectural languages, and Event-B.

It is also hoped that the plugin would improve readability of larger models: currently they are simply a long list of events with nothing except comments to provide any structuring clues.

Choices / Decisions

The primary functionality of the plugin is the generation of additional proof obligations. Rodin model builder automatically invokes the static checker and the proof obligations generator of the plugin and the proof obligations related to flow appear in the list of the model proof obligations.

One of the lessons learned with an initial plugin prototype was that a CSP-like language notation is not the best way to express event ordering as not all users are not familiar with process algebraic notations. It was decided to use graphical editor to would allow a visual layout of flow diagrams. This, in our view, is a more intuitive way of specifying event ordering. To realise this, we have relied on GMF: an Eclipse library for manipulating EMF models using graphical editors.

Available Documentation

There is a wiki page summarising proof obligation involved in proving machine/flow consistency.

Planning

The plugin is to be available for the time of release of Platform version 1.2.