Dynamic graphical UML views from formal B specifications

This paper addresses the graphical representation of the behaviour of B specifications, using state transition diagrams. These diagrams can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification authorities. The paper first discusses the principles of the graphical representation on a deterministic example, featuring a small set of states. It then discusses the representation of specifications which feature a large or infinite set of states, or which are non-deterministic. Abstraction techniques are used to overcome these difficulties. They result in a variety of possible representations. Finally, three techniques, based on animation and proof, are presented to help construct the diagrams.