Publications RSS Feed

UML-B: Formal modelling and design aided by UML

Snook, C. and Butler, M. (2006) UML-B: Formal modelling and design aided by UML. ACM Transactions on Software Engineering and Methodology 15(1) pp. 92-122.


pdfPDF - Requires Adobe Acrobat Reader or other PDF viewer.565Kb


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 requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilise a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specialisations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioural modelling. The design of UML-B has been guided by industrial applications.



ECS staff and postgraduates may modify this record.


Download Statistics

Last month

Last year

Members of ECS may view the download statistics dashboard for this record.


Metadata available via OAI as: oai_dc (unqualified dublin core)

The ECS EPrints Repository supports OAI 2.0 with a base URL of

EPrints is free software developed by the University of Southampton to facilitate Open Access to research.
  Welcome from Deputy Head of School (Research) Research Prospectus New Research Students Notes for Guidance New Research Students Notes for Guidance