Difference between pages "Tasking Event-B Tutorial" and "Tasking Event B Overview"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Andy
 
Line 1: Line 1:
For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk
+
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
  
<< I AM UPDATING THIS PAGE >>
+
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 [[#Implementing Events]]) to facilitate code generation.
  
=== Tasking Event-B Tutorial Overview ===
+
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.
 
 
This tutorial follows on from the abstract development described [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
 
 
 
This code generation tutorial extends the Heating Controller tutorial example, and makes use of example projects from the download site. The code generation stage produces Java code, and also an Event-B model. It is a model of the implementation, and contains flow control variables that model the flow of execution through the task body. The Java code is produced from an intermediate model that is not visible to the user. The Common Language model (CLM), is generated from the Tasking Event-B by a translation tool. Java (and other implementations) may be generated from the CLM. An overview of Tasking Event-B can be found [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview here].
 
 
 
In the example so far, the Heating Controller has been refined to the point where we wish to add implementation constructs. The Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines modelling tasks, shared objects and the environment are identified, and  extended with the appropriate implementation details.
 
 
 
The example/tutorial projects are are available from [https://github.com/andyed2003/codeGenExamples Git] or clone [https://github.com/andyed2003/codeGenExamples.git this].
 
  
 +
<center>
 
{| border="1"
 
{| border="1"
|Heating_ControllerTutorial2_Completed
+
|Construct
|An example project with an environment simulation. The environment variables are monitored and controlled using subroutine calls. The project contains a complete Tasking Development with generated Event-B and Java code.
+
|Options
 
|-
 
|-
|Heating_ControllerTutorial2_Partial1
+
|Machine Type
|A project with the final decomposition completed, ready to begin Tasking Event-B Development.
+
|DeclaredTask, AutoTask, SharedMachine
 
|-
 
|-
|Heating_ControllerTutorial2_Partial2
+
|Control
|A partially completed tasking specification for the continuation of the tutorial.
+
|Sequence, Loop, Branch, EventSynch
 
|-
 
|-
|TheoriesForCG
+
|Task Type
|Contains the mathematical language translations; encoded as rules in a theory plug-in rule-base.
+
|Periodic(n), Triggered, Repeating, OneShot
 +
|-
 +
|Priority
 +
| -
 +
|-
 +
|Event Type
 +
|Branch, Loop, ProcedureDef, ProcedureSynch
 +
|-
 +
|Parameter Type
 +
|ActualIn, ActualOut, FormalIn, FormalOut
 
|}
 
|}
 +
</center>
  
== Using the Tasking Extension ==
+
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 steps needed to generate code from an Event-B model, in this tutorial, are as follows,
 
* Step 1 - [[Tasking Event-B_Tutorial#Adding the Implementation Level Refinement|Adding the Implementation Level Refinement]]
 
* Step 2 - [[Tasking Event-B_Tutorial#Pre-processing|Pre-processing]]
 
* Step 3 - [[Tasking Event-B_Tutorial#Adding Tasking Event-B|Add Tasking annotations]].
 
* Step 4 - [[Tasking Event-B_Tutorial#Invoking the Translation|Invoke translators]].
 
=== Download and Copy the Theories ===
 
The translations of the Event-B mathematical language to the target language constructs are specified as rules in the theory plug-in. Example rule files are included for the example, and are available in MathExtension from the [https://github.com/andyed2003/codeGenTheoryRepo Git] repository, or clone [https://github.com/andyed2003/codeGenTheoryRepo.git this]. After checking out the theories, they must be un-deployed, then re-deployed, ensuring that the builder creates all of the appropriate files. Right-Click on the theory file and select deploy to do this. If you already have a MathExtensions folder then it should be renamed else the import will be prevented. Files from this folder can be copied and deployed in the new folder if necessary.
 
 
 
=== Adding the Implementation Level Refinement ===
 
The final decomposition generates the machines that are required for code generation. However, it is not possible to edit the machines since they are machine generated, and therefore this is prohibited. In order to be able to modify the models we will refine the generated machines. This is where we begin with the ''Heating_ControllerTutorial2_Partial1'' project (Where the pre-processing steps, described below, have been performed already). To refine the machines we can use the automatic refinement feature, but this presents us with two problems that are dealt with in the pre-processing steps.
 
 
 
=== Pre-processing ===
 
 
 
The pre-processing step, described here, is done automatically by the tool. The description is provided to assist with understanding the changes that occur to a model, during the code generation phase.
 
 
 
* The Code Generator requires a flattened, and annotated, version of each machine; all of the Event-B elements are made available in the implementation level machine.
 
 
 
===== 'Flattening' the Implementation Machines =====
 
 
 
* Events are changed to be ''not extended''.
 
* Abstract invariants are copied to the implementation level machine.
 
 
 
===== Annotations are provided automatically =====
 
 
 
* Typing annotations are added to typing invariants and axioms where they type variables and constants.
 
* Parameter directions (in or out) are inferred from the events.
 
 
 
=== Manually correcting the Composed Machine ===
 
 
 
The hierarchy created by successive machine decompositions gives rise to a tree of refined events. Only the leaf event nodes are used during code generation. In the current code generator there is no algorithm to navigate this tree automatically. Therefore the composed machine points to the incorrect machines and events.
 
 
 
We must manually change the composed machine to address this problem.
 
 
 
* Modify the lowest level decomposed machine, HCtrl_M1_cmp, to ''include'' the implementation level machines (task names ending in *Impl). To do this,
 
* open the composed machine editor. Open the INCLUDES edit feature.
 
* Select the second drop-down box and find the *Impl version of each machine.
 
* Save the composed machine.
 
* Now add missing synchronizations to the composed machine. Add the ''Envir1Impl'' to the includes of HCtrl_M1_cmp.
 
* Each composed event in the task, that synchronizes with the Environ machine, must have the remote event synchronization added manually. This can only be done by inspection of each composed event. We need to update Sense_Temperatures, Display_Current_Temperature, Actuate_OverHeat_Alram, Actuate_Heat_Source, Sense_Heater_Status, Actuate_NoHeat_Alarm, Sense_PressIncrease_Target_Temperature, Sense_PressDecrease_Target_Temperature, Display_Target_Temperature. One by one, expand the events in the composed events section of the composed machine editor; add a new event in the combines events section, select ''Envir1Impl'' and add the synchronizing event from the list-box to the right.
 
 
 
=== Removing Non-deterministic Constructs ===
 
 
 
It is also at this stage that any remaining non-deterministic constructs should be removed by replacing them with deterministic constructs.
 
 
 
TIP: Non-deterministic constructs cause strange characters to appear in the source code. If you see strange characters in the generated code, check for non-deterministic constructs in the implementation level machines.
 
 
 
Alter_Temperature_Sensor1 in Envir1Impl: action becomes ts1 := ts1 + 1
 
Alter_Temperature_Sensor2 in Envir1Impl: action becomes ts1 := ts1 + 1
 
Alter_Heater_Status in Envir1Impl: action becomes hss := FALSE
 
INITIALISATION in Heater_Monitor_TaskImpl: becomes shs := FALSE
 
 
 
=== Adding Tasking Event-B ===
 
 
 
*Setting Context attributes.
 
**Using the project ''Heating_ControllerTutorial2_Partial1''.
 
**Open the context, select the Tasking Context drop-down box, and select Tasking, as the type for the context.
 
 
 
Each Machine should be completed as follows.
 
==== The Temp_Ctrl_TaskImpl Machine ====
 
During this part of the tutorial we will cut and paste from ''Heating_ControllerTutorial2_Completed'' model when, specifying the task bodies, to save typing. We use the 'Event-B Machine Editor' to edit the Tasking Event-B.
 
 
 
*Add a Tasking element by clicking on the green + symbol next to Tasking.
 
*The machine type defaults to ''Auto Task''.
 
 
 
''Auto Tasks'' are tasks that will be declared and defined in the ''Main'' procedure of the implementation. The effect of this is that the ''Auto Tasks'' are created when the program first loads, and then activated (made ready to run) before the ''Main'' procedure body runs.
 
 
 
**Open The Tasking section of the Event-B editor.
 
**Click on + to add a new Task Type construct.
 
**Open Task Type (click on |> right arrow) in the Machine Type element.
 
**The task type defaults to ''Periodic'',
 
**Set a period of 250 milliseconds.
 
 
 
*'''Add a new TaskBody'''.
 
**Add a new Task Body section.
 
**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_TaskImpl''
 
**Save the model. Ignore the highlighted typing errors, since these annotations will be added by the code generator during pre-processing.
 
 
 
==== The Shared Machine ====
 
 
 
The next step is to identify the ''Shared_ObjectImpl'' machine as a ''Shared Machine''.
 
*Open the Tasking Section.
 
*Add a Machine Type by clicking +.
 
* Select ''Shared'' in the Machine Type drop Down box.
 
 
 
==== The Environ Machine ====
 
We identify the ''Envir1Impl'' as an ''Environ Machine'',
 
 
 
*Click on +,  in the Machine Editor, to add a to add a Tasking Section.
 
*A Machine Type element is created.
 
*Select ''Environ Machine'' in the drop down box.  
 
  
In the implementation, ''Environ Tasks'' are declared and defined in the ''Main'' procedure . The ''Envir1Impl'' machine models a task that simulates the environment, and can be used to generate simulation code. For deployment in a non-simulated environment the environ machine's generated code can be ignored. To specify the Environment task's behaviour we add edit the task body.
+
=== 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.
  
*'''Add the Task Details'''.
+
* Tasking Machines may be characterised by the following types:
**Open the Task Type section.
+
** AutoTasks - Singleton Tasks.
**Set the task type to ''Periodic'',
+
** Declared tasks - (Not currently used) A task template relating to an Ada ''tasktype'' declaration.
**Set a period of 100 milliseconds.  
+
** TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
**Add a new Task Body by clicking + in the Task Body section
+
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Envir1Impl''
 
**Save the model.
 
**Resolve any problems that are highlighted.
 
  
When saving, the task body text is sent to the parser. If parsing is successful then a builder adds the structure to the underlying EMF tree. If parsing fails then an error panel displays the source of the error.
+
=== Shared Machines ===
<!-- The final step is to complete the ''Sense_Temperatures'' event. The event, being a kind of synchronization, synchronizes with the ''Sense_Temperatures'' event in the ''Temp_Ctrl_Task'' tasking machine. We annotate the model with sensing and actuating implementation types.
+
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.
  
*'''Add a Sensed Event Annotation'''.
+
* Applied to the Shared Machine we have:
** Right-click on the ''Sense_Temperatures'' Event node.
+
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
** Select ''New Child/Implementation'' from the menu.
 
** Go to the Implementation properties view and set the ''Implementation Type'' property to ''Sensing''.
 
  
*'''Add an Actuating Event Annotation'''.
+
=== Tasks and Events ===
** Right-click on the ''Display_Current_Temperatures'' Event node.
+
==== Control Constructs ====
** Select ''New Child/Implementation'' from the menu.
+
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.  
** Go to the Implementation properties view and set the ''Implementation Type'' property to ''Actuating''.
 
-->
 
  
=== A Summary of Steps ===
+
* We have the following constructs available in the Tasking Machine body:
For a Tasking Machine definition:
+
** Sequence - for imposing an order on events.
# Select the Tasking Machine type (Auto etc).
+
** Branch - choice between a number of mutually exclusive events.
# Set the task type (Periodic etc.).
+
** Loop - event repetition while it's guard remains true.
# Set the task priority.
+
** 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.
# Specify the task body.
+
** 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.
<!-- # For sensing/actuating events, add the Event Type. -->
 
  
For a Shared Machine definition:
+
==== Implementing Events ====
# Add the ''SharedMachine'' Machine type.
+
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.
  
For an Environ Machine definition:
+
* Event implementation.
# Make the type an Environ Machine type.
+
** Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions are mapped to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.  
# Set the task type Periodic; a shorter period than the shortest task period is best for simulation.
+
** 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.  
# Set the task priority.
+
** 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.
# Specify the task body, it will contain a simulation of changes in the environment.
+
** 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 .
# For each sensing/actuating event, add the Event Type.
 
  
== Invoking the Translators ==
+
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:
  
* To generate Ada code,
+
* Event parameter types
** Right-Click on the composed machine, or any tasking machine in the development, select ''Code Generation/Translate Event-B to Ada''.
+
** FormalIn or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
** Open the generated ''code'' directory in the project to view the source files. A refresh will be necessary to make the code visible. The .gpr file has been provided for AdaCore GPS users.
+
** ActualIn or ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.
  
* To create the Event-B model of the implementation,
+
== References ==
** Right-Click on the composed machine, or any tasking machine in the development, select ''Code Generation/Translate Tasking Event-B to Event-B''.
 
** The Event-B model should be updated with the flow control variables. Users are not able to manually edit the generated elements. The additions can be removed using the menu option ''Code Generation/Remove Generated Event-B''
 
  
=== Generated Code ===
+
<references/>
Generated code will be visible in the code directory, in the Event-B project. However a refresh of the workspace is required. The directory is visible in the resource view; or alternatively, click on the view menu in the Event-B perspective, select customize view, and uncheck the ''all file and folders'' filter.
 
[[Category:User documentation]]
 

Revision as of 10:41, 10 December 2010

The following text can be read in conjunction with the slides[1] 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 #Implementing Events) 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 are mapped 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 or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
    • ActualIn or ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.

References