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... To facilitate and encourage the use of formal methods in industry. To do this we offer support to industrial partners in the form of training, advice and consultancy and at the same time develop the methods and tools to improve their usability. Particular tools and/or model to model translations can also be developed to meet specific customer the needs.