UML-B – Formal modelling with UML
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:
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:
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
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
Some work with Kim Sandström of Nokia Research Centre on using UML-B to model digital circuit components is described in
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
A control system was developed (with Walden and Tsiopoulos) as a case study.
Earlier versions of UML-B are described in:
4th January 2005