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:
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:
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