UML-B: A Plug-in for the Event-B Tool Set

UML-B provides a graphical front end for Event-B. It adds support for class-oriented and state machine modelling. UML-B is similar to UML but has its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools. When a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram. We introduce the UML-B notation, tool support and integration with Event-B. UML-B is a graphical formal modelling notation based on UML [1]. It relies on Event-B [2] for its underlying semantics and is closely integrated with the Event-B verification tools [3]. UML-B and Event-B are implemented within the Eclipse [4]

• Type: Conference
• Year: 2008
• Where: ASM
• Authors: Colin F. Snook, Michael J. Butler
• Keywords: ASM 2008, Computational Biology, Event-B Verification Tools, Tools, UML-B Provides