TY  - CONF
ID  - deploy435
UR  - http://eprints.soton.ac.uk/268261/
A1  - Savicks, Vitaly
A1  - Snook, Colin
A1  - Butler, Michael
Y1  - 2009/11//
N2  - Animation is important because it allows the modeller to validate that a model behaves as intended. Visualisation of animations assists the modeller in making this assessment. UML-B is a visual 'front-end' to the Event-B notation and includes a state-machine diagram editor. Here we describe a new plug-in which, using the Pro-B model checker as animation engine, provides animation of UML-B state-machine diagrams. Multiple diagrams can be animated simultaneously so that the behaviour of refinements and/or nested state-machines can be explored. 
TI  - Animation of UML-B State-machines
AV  - none
M2  - Dusseldorf
T2  - Rodin workshop, 2009
ER  -

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>