D23 UML-B

Overview

This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.

A new plug-in feature has been developed to provide Animation of UML-B State-machine diagrams. This feature was developed by University of Southampton.

The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Duesseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.

Motivations

This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.

UML-B improvements

The current version of the UML-B tool has been improved to support the refinement of State-machines. At the last deliverable, refinement of Classes was supported and State-machine refinement was beginning to be investigated. The investigation experimented with several notation and methodological alternatives. The design has now been finalised and an implementation has now been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of transition elaboration has been invented to represent this relationship.

Many other minor improvements have been made to the UML-B tool including: collapsing empty compartments on diagrams, improved navigation between diagrams, improved properties views ability to order classes and class-types in the translation support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems)

UML-B State-machine Animation

This feature was developed in response to a requirement from Seimens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

Choices / Decisions

This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

Available Documentation

This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:

• Requirements.
• Pre-studies (states of the art, proposals, discussions).
• Technical details (specifications).
• Teaching materials (tutorials).
• User's guides.

A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.

Planning

This paragraph shall give a timeline and current status (as of 29 Jan 2010).