IUML-B

iUML-B is a collection of diagrammatic editors for Event-B. The diagrams are contained within the machines they contribute to and are used to elaborate the machine and its content with extra model features.

• State-machine diagrams a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.

• Class diagrams a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets. An animator is also provided to visualise the progress of the state-machine.