UML-B – Formal modelling with UML

Michael Butler, Colin Snook

The emergence of the UML as a de-facto standard for object-oriented modelling has been mirrored by the success of the B method as a practically useful formal modelling technique. The two notations have much to offer each other. The UML provides an accessible visualisation of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but many software engineers find the notation difficult to learn, visualise and communicate.

We have developed a profile of the UML called UML-B that provides a, UML based, formal modelling notation supported by an action and constraint language derived from Abrial’s B method.  A description of UML-B can be found here:

UML-B: Formal modelling and design aided by UML.

Tool support for validation and verification of UML-B models is provided by translation to B. This enables the B animation, model checking and proof tools to be used. We provide a translator called U2B that converts a UML-B model into its equivalent B specification. The current version of U2B is a Rational Rose script. You can download the U2B translator, an example and a description here:

U2B Downloads

Our current work is to redevelop the U2B translator as an eclipse plug-in. This work is being carried out as part of the Rodin project. The plug-in will integrate with new B tools being developed at ETH Zurich. We are also redefining the UML-B profile based on the UML2 metamodel plug-in.

We are working closely with AT Engine Controls Ltd. (another partner in the Rodin project) on a case study that uses UML-B in the development of the failure management task of an engine control system. Preliminary results can be found in

Rigorous development of reusable, domain-specific components, for complex applications.

During the Pussee project we developed UML-B to support the specification of embedded system using the event B methodology. This work is described in

UML-B Specification for Proven Embedded Systems Design

Some work with Kim Sandström of Nokia Research Centre on using UML-B to model digital circuit components is described in

Using UML-B and U2B for formal refinement of digital components.

During the Matisse project we developed UML-B to support UML based modelling of B-action systems. B-action systems are a representation, using B, of the action systems formalism of Back. This work was carried out with Marina Walden of Abo Akademi and is described in

Use of U2B for specifying B action systems

A control system was developed (with Walden and Tsiopoulos) as a case study.

A case study in requirement analysis of control systems using UML and B

Earlier versions of UML-B are described in:

Using a Graphical Design Tool for Formal Specification,

Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit and

Using UML Class Diagrams for Constructing B Specifications.

4th January 2005