Difference between pages "Single View Design" and "Tasking Event-B Overview"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m (→‎Content: No more theorems in view customization, subsequently to "Theorems everywhere".)
 
imported>Andy
 
Line 1: Line 1:
−
==Purpose==
+
=== Tasking Event-B ===
 +
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 project that is suitable for a Tasking Development. During the modelling phase parameters are introduced to facilitate decomposition. As a result of the decomposition process, parameters become part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code generation. The tasking extension consists of the constructs in the following table.
  
−
The Rodin platform, at the beginning of the Deploy project, provided two views for displaying models and proofs:
+
<center>
−
* The ''Project Explorer'' displays the modelling elements stored in the Rodin database.
+
{| border="1"
−
* The ''Obligation Explorer'' displays the proof obligations together with their proof state.
+
|Construct
 +
|Options
 +
|-
 +
|Machine Type
 +
|DeclaredTask, AutoTask, SharedMachine, Environ
 +
|-
 +
|Control
 +
|Sequence, Loop, Branch, EventSynch
 +
|-
 +
|Task Type
 +
|Periodic(n), Triggered, Repeating, OneShot
 +
|-
 +
|Priority
 +
| -
 +
|-
 +
|Event Type
 +
|Branch, Loop, ProcedureDef, ProcedureSynch, Actuating, Sensing
 +
|-
 +
|Parameter Type
 +
|ActualIn, ActualOut, FormalIn, FormalOut
 +
|-
 +
|Addressed Variable
 +
|Address, Base
 +
|}
 +
</center>
  
−
The clean separation between modelling and proving looked good during paper design. However, users reported that they were constantly switching between the two views. This is due to the fact that modelling and proving are not separate activities, one being performed after the other. In general practice, both activities are intertwined.
+
=== Tasking Developments ===
 +
A Tasking Development is modelling component that is generated programmatically, at the direction of the user. The Tasking Development consists of a number of machines (and perhaps associated contexts). We make use of the Event-B EMF extension mechanism <ref name = "EBEMF">[[EMF framework for Event-B]]</ref>, which allows addition of new constructs to a model. 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.
  
−
Independently, Eclipse has released a new framework called the ''Common Navigation Framework'' since these two views were designed and implemented. The purpose of this framework is to provide Eclipse plug-ins with basic blocks for easily implementing views like the ''Project Explorer''. Moreover, this framework allows various plug-ins to cooperate together in populating such views, thus reinforcing plug-in integration into the platform.
+
==== 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.
  
−
Therefore, it was decided in the Deploy project to combine the two original views into a single one that would display modelling elements and proof obligations together. This new single view should also take advantage of the ''Common Navigation Framework'', in order to improve its seamless integration within Eclipse.
+
* 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. The period of a task is specified in milliseconds.
 +
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled. For the demonstrator tool the default priority is 5.
  
−
==Specification==
+
''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.
−
The Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework] that is provided by Eclipse.
 
  
−
===The Navigator===
+
==== Shared Machines ====
−
The navigator contains a tree of all projects and their contents. The users can choose between two ways how the machines and contexts will be presented:
+
A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.
−
*A simple structure where all machines and contexts are presented on the same level
 
−
*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
 
  
−
===The Statistics===
+
* Applied to the Shared Machine we have:
−
The statistics view presents information about the state of the proof obligations of the selected node in the navigator.
+
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
  
−
==User guide==
+
==== The Environ Machine ====
−
===Customizing the Navigator===
+
An Environ machine is a model of the environment. It can be used to generate code for use in a simulation, or discarded (from the IL1 model) in the case that a simulated environment is not required.
−
Click on the little triangle in the upper right corner of the navigator view and select ''Customize View''. This opens a dialog that allows you to choose ''Filters'' and ''Content''.
 
  
−
[[Image:Customize.jpg]]
+
* Applied to the Environ Machine we have:
 +
** An Environ Machine ''keyword'' that identifies a machine as an Environ Machine.
  
−
====Content====
+
=== Implementation Specifics ===
−
Here you can choose what content should be shown in the navigator.
+
At the stage where we are considering how to implement the Event-B development we need to think about controlling the flow of execution, and how events should be implemented. The following section describes the constructs that we have introduced to facilitate this.
−
*'''Resources''': All projects, files and folder (keep this one checked!).
+
==== Control Constructs ====
−
*'''Working Sets''': Allows you to see the working sets as top level elements. If you're not familiar with working sets, consult [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.user/concepts/cworkset.htm eclipse help].
+
Each Tasking Machine has a ''task body'' which contains the flow control (algorithmic constructs).  
−
*'''Simple Context Structure''': Lists all contexts of a project.
 
−
*'''Complex Context Structure''': Lists all contexts of a project. Contexts that extend another context are attached to it as children in the tree. Contexts that are seen by a machine are attached to the machine as children. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
 
−
*'''Simple Machines Structure''': Lists all machines of a project.
 
−
*'''Complex Context Structure''': Lists all machines of a project. Machines that refine another machine are attached to it as children in the tree. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
 
−
*'''Carrier Sets'''
 
−
*'''Constants'''
 
−
*'''Variables'''
 
−
*'''Axioms'''
 
−
*'''Invariants'''
 
−
*'''Events'''
 
−
*'''Proof Obligations''': All proof obligations of a machine, context, axiom, invariant, theorem or event.
 
  
−
Here is an example of what the same project looks like when using the complex machine and context structure (left) and when using the simple version (right).
+
* 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 two events.
 +
** Output - writes textual output to the screen.
  
−
[[Image:Complex.jpg]][[Image:Simple.jpg]]
+
Synchronization corresponds to:
 +
* a subroutine call from task to shared machine, or,
 +
* sensing or actuating of environment variables.
  
−
====Filters====
+
In the case of a subroutine call the subroutine is an atomic (with respect to an external viewer) update to state. 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.
−
The filters let you choose what to hide in the navigator.
 
−
*'''File types''': There are various filters to hide certain types of files.
 
−
*'''All files and folders''': Hides all files and subfolders.
 
−
*'''Non Rodin Projects''': Hides all non Rodin projects. Also hides closed Rodin Projects.
 
−
*'''Closed Projects''': Hides all closed projects.
 
  
−
There are some additional filters that can be found on top of the navigator:
+
In the case of a sensing or actuating event, the updates of the action correspond to reads of monitored variables, and writes to controlled variables of the environment.
  
−
[[Image:PoFilters.JPG]]
+
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, a Shared Machine that is visible to the task, or the Environ machine. Single events in a wrapper correspond to a subroutine call in an implementation.
  
−
Enter a text into the field and only proof obligations containing the string will be shown. If you push the green button, all discharged proof obligations will be hidden.
+
==== 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.
  
−
===Statistics===
+
* Event implementation.
−
The content displayed in the statistics view depends on the selection in the navigator. Generally it shows an overview of the status of all proof obligations of the selected elements and a more detailed view below (if available). If a project is selected this means that in the overview the statistics for all proof obligations of that project are shown. In the detailed viewed each machine and context is listed with their own statistics. If you double click on an element in the detailed view, the corresponding element will be selected in the navigator.
+
** 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.
 +
** ProcedureSynch - 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 .
 +
** Sensing - Identifies an event that maps to a read from the environment. If the environment is simulated without address variables then the sensing event is similar to a ProcedureSynch event, in that it has an update action that models assignment of a return value from a subroutine call. The event parameters act like the ''actualIn'' parameters of a ProcedureSynch event. On the other hand, if the event has addressed variables associated with its event parameters, then they map to direct reads from memory mapped variables in the generated code.
 +
** Actuating - Identifies an event that maps to a write to the environment. If the environment is simulated without address variables then the actuating event has no update action, the parameters act like ''actualOut'' parameters of a ProcedureSynch event. If a sensing event has addressed variables associated with its parameters then they map to direct writes to memory mapped variables in the generated code.  
  
−
It is possible to select multiple elements in the navigator and get a combined statistics. But the selected elements must be on the same level (e.g. projects, machines/contexts). This mean if you select both machines and projects at the same time, you won't get any statistics.
+
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:
  
−
==Developer guide==
+
* Event parameter types - Note: formal parameters are place-holders in a subroutine; they are replaced by the actual parameters at call time.
−
===Extending Single View Design===
+
** FormalIn or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
−
Single View Design uses the [http://wiki.eclipse.org/index.php/Common_Navigator_Framework Common Navigator Framework]. You can add custom filters, content providers and action providers in a plug-in of your own. Add the extension <code>org.eclipse.ui.navigator.viewer</code>. There you can add viewerContentBindings and viewerActionBindings with viewerId <code>fr.systerel.explorer.navigator.view</code>. This binds your custom content, actions and filters to the navigator.  
+
** ActualIn or ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.
  
−
In the picture you can see what types the nodes in the navigator have.
+
===== Addressed Variables =====
 +
When sensing monitored variables, or actuating controlled variables in the environment, we may wish to use explicit memory addresses for use in the final implementation, or perhaps in the environment simulation too. We can link a task's event parameters, and an Environ machines variables, with specific addresses and use these in the generated code.
  
−
[[Image:Tree.jpg]]
+
== References ==
  
−
====Adding a content provider to the navigator====
+
<references/>
−
To add a custom content provider you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new navigatorContent. Example: You want to add a new child under the IMachineRoot nodes. Define a navigatorContent and add triggerPoints. There you add a new <code>instanceof</code> with value <code>org.eventb.core.IMachineRoot </code>. The priority of the navigatorContent decides in what order the content is shown with respect to other content providers. (For example the content provider for the variables has a higher priority than the one for invariants, that's why the variables appear before the invariants in the tree.) You need to provide a contentProvider and a labelProvider class. Finally include your navigatorContent in your viewerContentBindings. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. There is a example project in the SVN repository, that adds a content provider to the navigator.
 
  
−
<code>
 
−
  <extension
 
−
        point="org.eclipse.ui.navigator.navigatorContent">
 
−
      <navigatorContent
 
−
            contentProvider="example.ContentProvider"
 
−
            id="example.navigatorContent"
 
−
            labelProvider="example.LabelProvider"
 
−
            name="Example Content">
 
−
        <triggerPoints>
 
−
            <instanceof
 
−
                  value="org.eventb.core.IMachineRoot ">
 
−
            </instanceof>
 
−
        </triggerPoints>
 
−
      </navigatorContent>
 
−
  </extension>
 
−
</code>
 
−
 
−
<code>
 
−
  <extension
 
−
        point="org.eclipse.ui.navigator.viewer">
 
−
      <viewerContentBinding
 
−
            viewerId="fr.systerel.explorer.navigator.view">
 
−
        <includes>
 
−
            <contentExtension
 
−
                  pattern="example.navigatorContent">
 
−
            </contentExtension>
 
−
        </includes>
 
−
      </viewerContentBinding>
 
−
  </extension>
 
−
</code>
 
−
 
−
====Adding a filter to the navigator====
 
−
To add a custom filter you have to use the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new commonFilter. You can either provide an implementation for <code>ViewerFilter</code> or use xml filterExpressions. For more information read the extension point description of [http://help.eclipse.org/help32/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/extension-points/org_eclipse_ui_navigator_navigatorContent.html navigatorContent]. Finally include your commonFilter in your viewerContentBindings. There is a example project in the SVN repository, that adds a filter to the navigator.
 
−
 
−
====Adding an action provider to the navigator====
 
−
To add a custom filter you use again the <code>org.eclipse.ui.navigator.navigatorContent</code> extension. There you add a new actionProvider. You have to provide an implementation for <code>org.eclipse.ui.navigator.CommonActionProvider</code>. To decide on what nodes in the tree your action provider should be invoked, use the enablement expression. Finally include your commonFilter in your viewerActionBindings. There is a example project in the SVN repository, that adds an action provider to the navigator.
 
  
 
[[Category:User documentation]]
 
[[Category:User documentation]]
−
[[Category:Developer documentation]]
 
−
[[Category:Design]]
 

Revision as of 15:30, 4 May 2011

Tasking Event-B

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 project that is suitable for a Tasking Development. During the modelling phase parameters are introduced to facilitate decomposition. As a result of the decomposition process, parameters become part of the interface that enables event synchronization. We make use of this interface and add information (see #Implementing Events) to facilitate code generation. The tasking extension consists of the constructs in the following table.

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

Tasking Developments

A Tasking Development is modelling component that is generated programmatically, at the direction of the user. The Tasking Development consists of a number of machines (and perhaps associated contexts). We make use of the Event-B EMF extension mechanism [1], which allows addition of new constructs to a model. 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. The period of a task is specified in milliseconds.
    • Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled. For the demonstrator tool the default priority is 5.

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.

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.

The Environ Machine

An Environ machine is a model of the environment. It can be used to generate code for use in a simulation, or discarded (from the IL1 model) in the case that a simulated environment is not required.

  • Applied to the Environ Machine we have:
    • An Environ Machine keyword that identifies a machine as an Environ Machine.

Implementation Specifics

At the stage where we are considering how to implement the Event-B development we need to think about controlling the flow of execution, and how events should be implemented. The following section describes the constructs that we have introduced to facilitate this.

Control Constructs

Each Tasking Machine has a task body which contains the flow control (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 two events.
    • Output - writes textual output to the screen.

Synchronization corresponds to:

  • a subroutine call from task to shared machine, or,
  • sensing or actuating of environment variables.

In the case of a subroutine call the subroutine is an atomic (with respect to an external viewer) update to state. 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.

In the case of a sensing or actuating event, the updates of the action correspond to reads of monitored variables, and writes to controlled variables of the environment.

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, a Shared Machine that is visible to the task, or the Environ machine. 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.
    • ProcedureSynch - 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 .
    • Sensing - Identifies an event that maps to a read from the environment. If the environment is simulated without address variables then the sensing event is similar to a ProcedureSynch event, in that it has an update action that models assignment of a return value from a subroutine call. The event parameters act like the actualIn parameters of a ProcedureSynch event. On the other hand, if the event has addressed variables associated with its event parameters, then they map to direct reads from memory mapped variables in the generated code.
    • Actuating - Identifies an event that maps to a write to the environment. If the environment is simulated without address variables then the actuating event has no update action, the parameters act like actualOut parameters of a ProcedureSynch event. If a sensing event has addressed variables associated with its parameters then they map to direct writes to memory mapped variables in the generated code.

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 - Note: formal parameters are place-holders in a subroutine; they are replaced by the actual parameters at call time.
    • 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.
Addressed Variables

When sensing monitored variables, or actuating controlled variables in the environment, we may wish to use explicit memory addresses for use in the final implementation, or perhaps in the environment simulation too. We can link a task's event parameters, and an Environ machines variables, with specific addresses and use these in the generated code.

References

  1. ↑ EMF framework for Event-B
Retrieved from ‘https://wiki.event-b.org/index.php?title=Single_View_Design&oldid=9648’