UML-B: Dependable Systems Modelling Language

Software defects result in a lot of time-consuming test and fix of software and, if left undetected, have a detrimental impact on software users. A significant proportion of software defects arise in requirements and design phases but are only detected after coding phases when software is being tested or deployed. The use of formal modelling to clearly specify and analyse requirements and designs helps to eliminate many defects prior to coding.



What is UML-B?


UML-B is a UML-like diagrammatic modelling notation that has a formal mathematical underpinning and supports incremental refinement. UML-B consists of class diagrams for modelling entity relationships and state-machines for modelling the behaviour of entities. UML-B models may contain invariant properties which are proven (via translation to Event-B) to always be true. For example, safety or security properties can be added as predicates in the diagrams and the behaviour of the system is proven to always maintain these properties. UML-B is based on Event-B and its supporting Rodin platform.

Event-B is a formal modelling language designed for rigorously modelling and verifying systems using abstraction and refinement. An Event-B model is a transition system where variables represent the state and events specify the transitions. Event-B uses a mathematical language that is based on set theory and predicate logic. Event-B is supported by the Rodin Platform, an extensible open source toolkit which includes facilities for modelling, verification (theorem proving and model checking) and validation (simulation).

  • Safety-Critical Systems
  • Security of Systems
  • Financially Critical Systems
  • Diagrammatic Modelling (UML style)
  • Verification by Proof
  • Validation by scenario Animation


Contact Us

umlb@soton.ac.uk

+442380599052



Recent Projects


DB Netz


DB Netz are using UML-B as a route to formal verification of digital Railway Command Control and Signalling (CCS) system specifications. In the EULYNX initiative, SysML specification models of CCS components have been developed such as an electronic interlocking and the corresponding field elements (point, signal, level crossing, etc.), describing their interfaces and how they communicate to make a safe railway system.

Click Here to find out more



Modelling the Hybrid ERTMS Level 3 in UML-B

We used UML-B to model and verify the safety of a new European railway specification, Hybrid ERTMS Level 3. The specification is for a new kind of control system that will allow new trains that can communicate their position, to operate alongside older trains that rely on track detection equipment.

The control system splits the existing track sections into virtual sections so that the newer trains can be run at closer intervals, but reverts to using track detection in the presence of older rolling stock. We used UML-B class diagrams to model the relationships between trains and track sections and state-machines to model the state of trains. Our model was constructed using nine refinement levels, culminating in a UML-B state-machine representing the control system of the specification.

Click Here to find out more