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.