"435","Animation of UML-B State-machines","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. ","http://deploy-eprints.ecs.soton.ac.uk/435/","Savicks, Vitaly and Snook, Colin and Butler, Michael","UNSPECIFIED","       <span class=\"person_name\">Savicks, Vitaly</span> and <span class=\"person_name\">Snook, Colin</span> and <span class=\"person_name\">Butler, Michael</span>     (2009)  <a href=\"http://deploy-eprints.ecs.soton.ac.uk/435/\"><em>Animation of UML-B State-machines.</em></a>       In: Rodin workshop, 2009, Dusseldorf.           ","","2009-11"
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>