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

UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:-

A tutorial on how to refine state-machines is available on the wiki: Refinement_of_Statemachines

State-machine animation is described on the wiki here:- UML-B_-_Statemachine_Animation

It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18261/

The EMF Framework for Event-B is described on the wiki here:- EMF_framework_for_Event-B

It is also available as a short paper here:- http://eprints.ecs.soton.ac.uk/18262/

Planning

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