Difference between pages "D32 Code generation" and "Event-B Classdiagrams"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Colin
 
Line 1: Line 1:
'''THIS DOCUMENT IS NOT YET COMPLETE !!!'''
+
[[Image:IUMLB_big.png|frame|left]]
 +
{{TOCright}}
 +
==Introduction==
 +
In iUML-B, Class diagrams are used to define and visualize entity-relationship data models. They can be added to Event-B Machines and Event-B Contexts and visualize given sets , constants and variables. Diagram elements elaborate pre-existing user data in order to visualize it. The diagram defines type, sub-type and further constraint information for the data by generating invariants or axioms.
  
== General Overview ==
+
==Principles of Operation==
  
The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">http://wiki.event-b.org/index.php/Event_Model_Decomposition</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">http://wiki.event-b.org/index.php/EMF_framework_for_Event-B</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">http://wiki.event-b.org/index.php/Flows </ref> and the algorithmic structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.
+
Classes, Attributes and Associations are all model elements that represent data. They can be linked to existing Event-B data elements: Variables, Constants or (for Classes only) Carrier Sets. This relationship is called ''Elaborates'' because the diagram element elaborates properties of the data item. Any data element within scope, locally within the same machine or context, or via sees and extends, can be elaborated. As a short cut, a button is provided to create a new data item and link to it in one step.  
  
== Motivations ==
+
Class diagrams can be added to Machines or Contexts, but note that some features are not available when in a Context (e.g. only constants and sets are within scope to link to and methods cannot be used in classes).
  
The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> http://wiki.event-b.org/index.php/D23_Code_Generation </ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.
+
Methods can be placed inside Classes and link (elaborate) one or more events in the containing Machine. This means that the elaborated events are given a paramter representing the class instance (similar to 'this' or 'self' in programming languages). When in variable classes (i.e. a class that elaborates a variable) methods may be constructors or destructors.
  
== Choices / Decisions ==
+
===Main Data Elements of a Class Diagram===
=== Strategic Overview ===
+
The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize Event-B data items (carrier sets, constants or variables) in the Event-B model. Only a class can visualize a carrier set. The class diagram also visualizes the relationships between these data items and generates constraints (invariants and axioms as appropriate) as follows.
During the last year we have focussed on supporting the generation of code for typical real-time embedded control software. To this end we have evolved a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Individual tasks are treated as sequential programs; these tasks are modelled by an extension to Event-B, called ''Tasking Machines''. Tasks have mutually exclusive access to state variables through the use of protected resources. The protected resources correspond to Event-B machines. For real-time control, periodic and one-shot activation is currently supported; and it is planned to support aperiodic tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software. For the DEPLOY project, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated.  
+
* '''Class Supertype''' relationships between classes represent that the source is a sub-set of the target superset.  
 +
* '''Association''' relationships represent that the association data is a relation between instances of the source and target classes. Cardinality may be used to further constrain the relationship to be for example a function, injection or surjection.
 +
* '''Attributes''' are similar to associations except that the target is given by a text string (the attribute type property).
  
Our main goal this year has been to devise an approach for, and provide tool support for, code generation. In accord with the resources available during the year it was decided to limit the provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will allow interested parties to explore the approach.
+
===Other Elements of a Class Diagram===
 +
* '''Constraints''' can be added to classes. The constraint is automatically universally quantified for all instances of the class. The user is expected to use the class' ''self name'' to represent the quantifier local variable. (By default the self name is ''this_<className>'' but it can be altered in the properties of the class). The constraint will generate an axiom or an invariant depending on wheter the class diagram is owned by a context or machine.
 +
* For class diagrams that are owned by a machine, '''methods''' may be placed in classes. Methods are linked to events of the machine and a parameter is generated to represent the contextual instance, using the class' self-name. The user is expected to use the self name in guards and actions of the method. Note that the method-event elaborates relationship is many to many. Hence several methods in different classes could elaborate the same event. Conversely the same method may contribute its behaviour to several different events.
  
=== The Tasking Extension for Event-B ===
+
===Scope===
 +
Elements of the class diagram can define data in the containing Event-B component and can visualize data in any Event-B component that is visible to the containing Event-B component (including itself). Hence a class diagram in a context may visualize sets and constants in the containing context and visualize sets and constants in any context which is (transitively) extended by the containing context.  A class diagram in a machine may define/visualize variables in the containing machine, visualize variables in any machine it (transitively) refines and visualize sets and constants in any context that is seen by the machine or any Context that is (transitively) extended by a context that is seen by the machine.
  
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d108734/Andy%20Edmunds%20-%20Code%20Generation%20Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
+
===Secondary information===
 +
Colour is used to indicate whether a diagram element has been linked to data. Icons are used to indicate the kind (set, constant or variable) of elaborated data.
  
Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a tasking development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Events For Tasking]]) to facilitate code generation.
+
==Examples==
 +
For example when a class diagram is first drawn and has not been linked to data it looks like this:
  
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.
+
[[File:Cd1_unlinked.png]]
  
<center>
 
{| border="1"
 
|Construct
 
|Options
 
|-
 
|Machine Type
 
|Declared Task, AutoTask, Shared Machine
 
|-
 
|Control
 
|Sequence, Loop, Branch, EventSynch
 
|-
 
|Task Type
 
|Periodic(n), Sporadic, Repeating, One-shot
 
|-
 
|Priority
 
| -
 
|-
 
|Event Type
 
|Branch, Loop, ProcedureDef, ProcedureSynch
 
|-
 
|Parameter Type
 
|ActualIn, ActualOut, FormalIn, FormalOut
 
|}
 
</center>
 
  
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.
+
Generating this diagram produces no output to the Event-B.
 +
The diagram elements must first be linked to data using the '''Link Data''' or '''Create & Link''' buttons in the properties sheet.
 +
The followng screenshot shows the association being linked to a variable ''b'' that already exists in the machine.
  
=== More about Constructs ===
+
[[File:LinkData.png|800px]]
  
==== Control Constructs ====
 
  
* Applied to Tasking Machines we have:
+
The following screenshot shows the class A being used to create and link to a carrier set in the seen context X0. Note that the carrier set is created in X0 immediately. It is not necessary to generate.
** Sequence - for imposing an order on events.
 
** Branch - choice between a number of mutually exclusive events.
 
** Loop - event repetition while it's guard remains true.
 
** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine.
 
** Event-wrappers - The synchronization construct is contained in an event wrapper. The wrapper may also contain a single event which may belong to the Tasking Machine, or the Shared Machine.
 
  
* Applied to the Shared Machine we have:
+
[[File:CreatLink.png|800px]]
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
 
  
==== Events For Tasking ====
 
Event implementation. Branch, Loop, ProcedureSych, ProcedureDef
 
  
Event parameter types. FormalIn FormalOut, ActualIn, ActualOut
+
After linking these diagram elements they are automatically rendered differently including icons for variables (b) and sets (A). Generating at this stage introduces an invariant for the association variable b to say that it is a relation between A and B. Since B only exists in the diagram and is not yet linked to any data, this causes an error in the machine. However, note that the invariant is still generated using the class name, B. In fact we could replace the class name with any valid expression (e.g. NAT) representing a set of instances.
  
==== Tasking Machines ====
+
[[File:ClassDiagGen.png|800px]]
Auto-Tasks.
 
  
Declared tasks.
 
  
Task type.
+
In the following screenshot, B has been linked to a constant in the context X0. The supertype relation from B to A generates the axiom, B ∈ ℙ(A).
 +
A method (with a parameter, guard and action) and an invariant have been added to class A and their translations are shown in the machine m0.  
  
Task priority.
+
[[File:ClassDiagGen2.png|800px]]
 
 
==== Shared Machines ====
 
 
 
Events can only be ProcedureDef or ProcedureSynch
 
 
 
Parameters of ProcedureSynch can only be FormalIn or FormalOut
 
 
 
ProcedureDef - parameters not allowed.
 
 
 
 
 
=== Other Technical Issues ===
 
 
 
Meta-models: The use of Epsilon for translation.
 
 
 
=== The Deliverable ===
 
The demonstrator tool was released on 30 November 2010, and is available as an update site, or bundled Rodin package from:
 
https://sourceforge.net/projects/codegenerationd/files
 
 
 
Sources are available from:
 
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
 
 
 
The tool is based on a build of Rodin 1.3.1 (not Rodin 2.0.0 due to dependency conflicts).
 
 
 
* The Code Generation tool consists of,
 
** a tasking Development Generator.
 
** a tasking Development Editor (Based on an EMF Tree Editor).
 
** a translator, from Tasking Development to Common Language Model (IL1).
 
** a translator, from the Tasking Development to Event-B model of the implementation.
 
** a pretty-printer for the Tasking Development.
 
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
 
 
== Available Documentation ==
 
 
 
 
 
Much insight was gained during the work on code generation reported in the thesis ''Providing Concurrent Implementations for Event-B Developments'' <ref name="aeThesis">http://eprints.ecs.soton.ac.uk/20826/</ref>
 
 
 
Tooling issues were reported in a paper ''Tool Support for Event-B Code Generation''
 
<ref name = "toolSupport">http://eprints.ecs.soton.ac.uk/20824/</ref>
 
which was presented at ''Workshop on Tool Building in Formal Methods'',
 
http://abzconference.org/
 
 
 
There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.
 
 
 
=== For users ===
 
 
 
There is a wiki page at http://wiki.event-b.org/index.php/Code_Generation_Activity
 
 
 
There is a tutorial at http://wiki.event-b.org/index.php/Code_Generation_Tutorial
 
 
 
== Planning ==
 
 
 
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
 
 
 
== References ==
 
 
 
<references/>
 

Latest revision as of 05:07, 6 October 2015

IUMLB big.png

Introduction

In iUML-B, Class diagrams are used to define and visualize entity-relationship data models. They can be added to Event-B Machines and Event-B Contexts and visualize given sets , constants and variables. Diagram elements elaborate pre-existing user data in order to visualize it. The diagram defines type, sub-type and further constraint information for the data by generating invariants or axioms.

Principles of Operation

Classes, Attributes and Associations are all model elements that represent data. They can be linked to existing Event-B data elements: Variables, Constants or (for Classes only) Carrier Sets. This relationship is called Elaborates because the diagram element elaborates properties of the data item. Any data element within scope, locally within the same machine or context, or via sees and extends, can be elaborated. As a short cut, a button is provided to create a new data item and link to it in one step.

Class diagrams can be added to Machines or Contexts, but note that some features are not available when in a Context (e.g. only constants and sets are within scope to link to and methods cannot be used in classes).

Methods can be placed inside Classes and link (elaborate) one or more events in the containing Machine. This means that the elaborated events are given a paramter representing the class instance (similar to 'this' or 'self' in programming languages). When in variable classes (i.e. a class that elaborates a variable) methods may be constructors or destructors.

Main Data Elements of a Class Diagram

The main data elements of a class diagram are class, association and attribute. These elements all visualize Event-B data items (carrier sets, constants or variables) in the Event-B model. Only a class can visualize a carrier set. The class diagram also visualizes the relationships between these data items and generates constraints (invariants and axioms as appropriate) as follows.

  • Class Supertype relationships between classes represent that the source is a sub-set of the target superset.
  • Association relationships represent that the association data is a relation between instances of the source and target classes. Cardinality may be used to further constrain the relationship to be for example a function, injection or surjection.
  • Attributes are similar to associations except that the target is given by a text string (the attribute type property).

Other Elements of a Class Diagram

  • Constraints can be added to classes. The constraint is automatically universally quantified for all instances of the class. The user is expected to use the class' self name to represent the quantifier local variable. (By default the self name is this_<className> but it can be altered in the properties of the class). The constraint will generate an axiom or an invariant depending on wheter the class diagram is owned by a context or machine.
  • For class diagrams that are owned by a machine, methods may be placed in classes. Methods are linked to events of the machine and a parameter is generated to represent the contextual instance, using the class' self-name. The user is expected to use the self name in guards and actions of the method. Note that the method-event elaborates relationship is many to many. Hence several methods in different classes could elaborate the same event. Conversely the same method may contribute its behaviour to several different events.

Scope

Elements of the class diagram can define data in the containing Event-B component and can visualize data in any Event-B component that is visible to the containing Event-B component (including itself). Hence a class diagram in a context may visualize sets and constants in the containing context and visualize sets and constants in any context which is (transitively) extended by the containing context. A class diagram in a machine may define/visualize variables in the containing machine, visualize variables in any machine it (transitively) refines and visualize sets and constants in any context that is seen by the machine or any Context that is (transitively) extended by a context that is seen by the machine.

Secondary information

Colour is used to indicate whether a diagram element has been linked to data. Icons are used to indicate the kind (set, constant or variable) of elaborated data.

Examples

For example when a class diagram is first drawn and has not been linked to data it looks like this:

Cd1 unlinked.png


Generating this diagram produces no output to the Event-B. The diagram elements must first be linked to data using the Link Data or Create & Link buttons in the properties sheet. The followng screenshot shows the association being linked to a variable b that already exists in the machine.

LinkData.png


The following screenshot shows the class A being used to create and link to a carrier set in the seen context X0. Note that the carrier set is created in X0 immediately. It is not necessary to generate.

CreatLink.png


After linking these diagram elements they are automatically rendered differently including icons for variables (b) and sets (A). Generating at this stage introduces an invariant for the association variable b to say that it is a relation between A and B. Since B only exists in the diagram and is not yet linked to any data, this causes an error in the machine. However, note that the invariant is still generated using the class name, B. In fact we could replace the class name with any valid expression (e.g. NAT) representing a set of instances.

ClassDiagGen.png


In the following screenshot, B has been linked to a constant in the context X0. The supertype relation from B to A generates the axiom, B ∈ ℙ(A). A method (with a parameter, guard and action) and an invariant have been added to class A and their translations are shown in the machine m0.

ClassDiagGen2.png