UML-B Integration and Improvements

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 (Eclipse Modelling Framework (EMF)). "The EMF project is a modeling framework and code generation facility for building tools and other applications based on a structured data model". [1]

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.x) contains significant improvements, most notably the addition of support for refinement of state machines. New features include:

• Support for refinement of state machines in UML-B. This release allows a state machine 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 state machine can be elaborated by adding more detailed hierarchical state machines. This addition is described in more detail in Said, Butler and Snook

• Support for synchronisation of transitions from different state machines. This feature will allow two or more transitions in different state machines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case state machines) 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.

• An action (toolbar button and menu item) has been added to enable manual invocation of the UML-B to Event-B translation process. This can be used in place of the automatic builder for larger projects where frequent re-verification may be inconvenient.

• Synchronisation of different diagram editors and views has been improved.

• File maintenance has been improved so that diagrams and Event-B models are deleted when corresponding model elements are deleted.

• Logging (of internal errors and exceptions etc.) has been improved and now uses standard Eclipse error logging facilities.