Event-B Statemachines Plug-in is part of the iUML-B experimental tool that focuses on UML-B and Event-B integration. The plug-in provides a way of adding state machines directly to Event-B machines and is capable of translating former to Event-B language. It also offers a UML-like diagram editor for state machines, as well as state machine animation, which can be installed as additional plug-in that runs on top of ProB Animator.
The Event-B Statemachines plug-in is available for installation from Rodin update site under Modelling Extensions category. Animation plug-in for it is available from Verification and Validation category. Both plug-ins require EMF and GMF frameworks, Event-B EMF framework, ProB, OCL and QVT - all of these dependencies will be installed automatically upon plug-in installation.
Using the tool
The tool consists of a standard UML-like graphical editor for state machine diagrams, and integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.
To start the modelling all you have to do is to select a machine in Event-B Explorer that you would like to extend with state machines and click on Create new statemachine from explorer's toolbar. An input dialog will appear asking you for name of a new state machine. After that you should be able to see a new state machine appearing as a child of machine in explorer.
The explorer also shows the contents of state machines, including states, transitions and annotations. You can customise the amount if information you would like to see by going to explorer's menu (a small triangle at the top right-hand side) > Customize View.. > Filters tab. There are three filters defined for state machines: Annotation Filter, Transition Filter, State Filter - that hide corresponding elements in explorer (state filter hides simple states, like initial, final or ANY).
In addition, there are Open and Delete actions available for state machine in context menu of explorer. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key). In the machine context menu there are two more actions related to state machines: Refine with statemachines and Delete generated - which allow correspondingly to create a refinement of machine with state machine refinements (not available yet from standard Refine action of Rodin) and to delete all Event-B elements generated by state machines (required only for experimental purposes if generated things/diagrams get corrupted).
To edit a state machine in diagram editor you simply double-click it. The tool creates a diagram file for you with the same name as root state machine.
Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: States, State Features and State Links. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu Window > Show View > Properties). After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.
The diagram allows to create the following State elements:
- Refined State (shall not be used)
- Initial (state)
- Final (state)
- ANY (state)
A state can have nested state machines, added from State Features, which correspond to UML parallel substates, also called parallel (or orthogonal) regions.
Finally, states can have transitions from one to another, created from State Links. Transitions can also be created from popup arrows on states and link to either existing states or to ones created from the context menu.
There are some semantic rules that must be obeyed in order for a state machine model to be valid and translatable to Event-B. These rules are implemented in the validation framework and are checked either when validation is called explicitly from context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.
- Transition cannot go to initial state
- Transition cannot go from final state
- Transition cannot go directly from initial to final state
- Transition should elaborate an event if
- it is on the root state machine (its source/target belongs to root)
- it is in nested state machine and not initial or final (its source/target is initial or final state)
- Initial state should have outgoing transitions
- Final state should have incoming transitions
- Root state machine must have an initial state
- State machine can only have one initial state
- State machine can only have one final state
- State machine must have an initial state if
- its parent state has incoming transitions
- it has outgoing local transitions (going from a state to parent state or ANY state)
- Concrete state cannot contain refined state machines
- Concrete state machine cannot have refined states
- Refined state machine cannot have concrete states
Not all the rules are strict i.e. rule violation is considered as error - they are not causing translation problems, but keeping a model semantically correct means everything will be translated as intended.
The diagram editor, as mentioned, has two ways of checking the diagram model against these rules. After validation completes, it produces feedback in the form of a dialog, telling whether model is valid or has some errors. The elements that violate any rules are also marked with error/warning markers, which are listed in Problems view, as well as displayed on the diagram.
The context menu of a diagram includes four specific actions:
- Validate - to run the validation check on state machine model
- Translate to Event-B - to run the translation of state machine to Event-B language
- Start Animation - to run ProB animation and animate the diagram
- Stop Animation - to stop the animation and return to Event-B perspective