Difference between pages "UML-B FAQ" and "UML-B Integration and Improvements"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
 
imported>Colin
(New page: === UML-B Integration with Event-B=== UML-B provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visuali...)
 
Line 1: Line 1:
−
==How should I model a fixed set of instances with a class?==
+
=== UML-B Integration with Event-B===
  
−
It is often useful to use a class to model a small, fixed set of instances. (As opposed to an indeterminate variable set where instances are constructed dynamically).  
+
UML-B provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element.  However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (refines, sees and extends). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (EMF).
−
For example, to model a bridge between a mainland and an island, I would define a new class type BRIDGE and enumerate it with a constant, "myBridge"  (i.e. Instances = {myBridge} where {myBridge} has been added as a type expression using the add new type button).  I might also define the mainland and island this way as instances of a class type, LAND, and use an association to represent the connection of LAND to BRIDGE. (My model loses the generic distinction between mainlands and islands, so you might prefer to use 2 seperate classtypes). I would do all this in a Context diagram rather than a class diagram. That way it represents contextual configuration data, rather than  state variables.
 
  
−
[[Image:EnumeratedClassTypes.png]]
+
The integration between UML-B and Event-B will be improved by introducing an EMF framework for Event-B. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.
  
−
To specify the association exactly, I could add axioms to define the actual mapping of mainland and island to myBridge. However, be careful because if this specific data conflicts with the more general definition of bridges the prover will not work properly. (It would be better if the type axiom for bridges was minimal and the cardinality restrictions (bijection in this case) were made into Theorems to be proved).
+
===Improvements to the existing version of UML-B===
 +
While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:
  
−
In order to use these concepts in a class diagram (i.e. to add variables and events based on this configuration data) I would add corresponding classes and set their variability to fixed (because we don't want to model creation of land and bridges). To force them to have the same instances as the class types I add a new type expression for each class type, BRIDGE and LAND, and then set the corresponding class instances to these types. (Note that using supertype  would make the class instances into subsets of the configuration data which is not quite what we want here).
+
* Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in [[Said, Butler and Snook]]
  
−
[[Image:fixedClassInstances.png]]
+
* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
  
−
Of course, for this example, you could obtain a much simpler model by leaving out the explicit modelling of bridge, island and mainland, but the advantage of our model is that it can easily be extended to deal with different configurations having several bridges and islands.
+
* Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which was formerly denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
  
−
[[Category:User FAQ]]
+
* The properties view has been improved with the addition of a tab for 'model'. This tab allows direct access to the underlying EMF model element so that its properties can be viewed and changed.
−
[[Category:UML-B]]
+
 
 +
* Some improvements have been made to the UML-B perspective layout to reflect changes to the Event-B one. The task and problem views have been removed and the 'Rodin Problem' view has been added instead.

Revision as of 17:31, 16 December 2008

UML-B Integration with Event-B

UML-B provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element. However, many features of UML-B are a replication of corresponding Event-B features. For example, the project diagram in UML-B, uses the concepts of machines and contexts and their relationships (refines, sees and extends). The project diagram would be just as applicable to an Event-B project that did not use any UML like modelling concepts. Similarly, while modelling in UML-B class diagrams, model elements are introduced to a machine that are directly equivalent to their Event-B counterparts. Greater integration would allow UML-B diagrams to be interspersed with Event-B model elements in a flexible mixed modelling interface. This has not been possible due to the differing underlying technologies used for Event-B (bespoke data repository) and UML-B (EMF).

The integration between UML-B and Event-B will be improved by introducing an EMF framework for Event-B. This will allow UML-B to be re-implemented as an extension to Event-B. Work has begun on this framework and resulting integrated tools will become available during 2009.

Improvements to the existing version of UML-B

While this new UML-B is being developed, improvements to the existing version of UML-B are ongoing. A new release of UML-B (0.5.0)) contains significant improvements, most notably the addition of support for refinement of statemachines. New features include:

  • Support for refinement of state machines in UML-B. This release allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines. This addition is described in more detail in Said, Butler and Snook
  • Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
  • Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which was formerly denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
  • The properties view has been improved with the addition of a tab for 'model'. This tab allows direct access to the underlying EMF model element so that its properties can be viewed and changed.
  • Some improvements have been made to the UML-B perspective layout to reflect changes to the Event-B one. The task and problem views have been removed and the 'Rodin Problem' view has been added instead.
Retrieved from ‘https://wiki.event-b.org/index.php?title=UML-B_FAQ&oldid=10489’