Difference between pages "D23 Decomposition" and "Event-B Classdiagrams"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Colin
 
Line 1: Line 1:
−
= Overview =
+
''this page is under construction''
−
The Event-B model decomposition is a new feature in the Rodin platform.
+
[[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.
  
−
Two methods have been identified in the DEPLOY project for model decomposition: the ''shared variable'' decomposition (or A-style decomposition), and the ''shared event'' decomposition (or B-style decomposition). They both answer to the same requirement, namely the possibility to decompose a model <math>M</math> into several independent sub-models <math>M_1, ...,M_n</math>.
+
==Principles of Operation==
  
−
Academic (ETH Zurich, University of Southampton) and industrial (Systerel) partners were involved in the specification and development of model decomposition. Systerel, which could have useful discussions with Jean-Raymond Abrial on the topic, was more especially responsible for the A-style decomposition. The University of Southampton, where Michael Butler is professor, was in charge of the B-style decomposition.
+
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).
−
One of the most important feature of the Event-B approach is the possibility to introduce additional details such as new events and data during refinement steps.
 
  
−
Therefore, the refinement process entails an increasing complexity of a model, where one has to deal with a growing number of events, state variables, and consequently proof obligations.
+
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.
−
This is well illustrated in the ''Event build-up'' slide of the Wright presentation during the Rodin Workshop 2009.
 
−
: See [http://wiki.event-b.org/index.php/Image:Steve_Wright_Quite_Big_Model_Presentation.pdf Experiences with a Quite Big Event-B Model].
 
  
−
The purpose of the Event-B model decomposition is precisely to give a way to address such a difficulty, by cutting a large model <math>M</math> into smaller sub-models <math>M_1, ..., M_n</math>. The sub-models can then be refined separately and more comfortably than the whole. The constraint that shall be satisfied by the decomposition is that these refined models might be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>.
+
===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).
  
−
The model decomposition leads to some interesting benefits:
+
===Other Elements of a Class Diagram===
−
* Design/architectural decision. It applies in particular when it is noticed that it is not necessary to consider the whole model for a given refinement step, because only a few events and variables are involved instead.
+
* 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.
−
* Complexity management. In other words, it alleviates the complexity by splitting the proof obligations over the sub-models.
+
* 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.
−
* Team development. More precisely, it gives a way for several developers to share the parts of a decomposed model, and to work independently and possibly in parallel on them.
 
  
−
Note that the possibility of team development is among the current priorities for all industrial partners. The model decomposition is a first answer to this issue.
+
===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.
  
−
= Choices / Decisions =
+
===Secondary information===
−
The main decision concerning the implementation of the Event-B model decomposition in the Rodin platform is to make available both decomposition styles (''shared variables'' and ''shared events'') through one single plug-in. These approaches are indeed complementary and the end-user may take advantage of the former or of the latter, depending on the model, e.g., the ''shared variables'' approach seems more suitable when modelling parallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems.
+
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.
  
−
Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
+
==Examples==
−
* Planning. Some options, such as using the Graphical Modelling Framework for the decomposition visualization, or outsourcing the context decomposition, have not been explored (at least in the first instance), mainly because of time constraints (in the DEPLOY description of work, the decomposition support is planned for end of 2009).
+
For example when a class diagram is first drawn and has not been linked to data it looks like this:
−
* Easy-to-use (however not simplistic) tool. It applies on the one hand to the tool implementation (decomposition wizard, configuration file to replay the decomposition) and on the other hand to the tool documentation (the purpose of the user's guide is to provide useful information for beginners and for more advanced users, in particular through a ''Tips and Tricks'' section).
 
−
* Modularity and consistency. In particular, the developments have not been performed in the Event-B core. Instead the Eclipse extension mechanisms have been used to keep the plug-in independent (e.g., the static checker, the proof obligation generator and the editor have been extended).
 
−
* Performance. The decomposition tool should perform in reasonable time and memory, compared to other Rodin plug-ins.
 
−
* Recursivity. It must be possible to decompose a previously decomposed model.
 
  
−
Other technical decisions are justified in the specification wiki pages.
+
[[File:Cd1_unlinked.png]]
  
−
= Available Documentation =
 
−
The following wiki pages have been respectively written for developers and end-users to document the Event-B model decomposition:
 
−
* Shared variables (A-style) decomposition specification.
 
−
:See [http://wiki.event-b.org/index.php/Event_Model_Decomposition Event Model Decomposition].
 
−
* Decomposition plug-in user's guide.
 
−
:See [http://wiki.event-b.org/index.php/Decomposition_Plug-in_User_Guide Decomposition Plug-in User Guide].
 
  
−
= Planning =
+
Generating this diagram produces no output to the Event-B.
−
The decomposition plug-in is available since release 1.2 of the platform (initial version).
+
The diagram elements must first be linked to data using the '''Link Data''' or '''Create & Link''' buttons in the properties sheet.
−
:See [http://wiki.event-b.org/index.php/Rodin_Platform_1.2_Release_Notes Rodin Platform 1.2 Release Notes] and [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition Release History].
+
The followng screenshot shows the association being linked to a variable ''b'' that already exists in the machine.
  
−
[[Category:D23 Deliverable]]
+
[[File:LinkData.png|800px]]
 +
 
 +
 
 +
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.
 +
 
 +
[[File:CreatLink.png|800px]]
 +
 
 +
 
 +
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.
 +
 
 +
[[File:ClassDiagGen.png|800px]]

Revision as of 14:54, 5 October 2015

this page is under construction

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=D23_Decomposition&oldid=4058’