Refinement of Statemachines

Return to UML-B

This example of an ATM (automated teller machine) shows the techniques used to make a refinement of a state machine. The example uses a machine-level state machine (i.e. not in a class). The state machines use the state-sets translation which, since there are no class instances, results in each state being represented by a boolean variable.

1. Create a new UML-B project using the New-UML-B Project Wizard
2. Create a machine called ATM_A using the package diagram palette Machine tool
3. Open its class diagram by selecting the machine and then clicking the button in the properties view (or using the pop-up menu).
4. Add a statemachine called atm_sm to the canvas using the diagram palette Statemachine tool.
5. Open the state machine and draw the state machine model shown in the diagram below using the statemachine diagram palette.

The statemachine models an ATM which has 2 states, idle (not in use) and active. The ATM starts off in the state idle. When a card is inserted, represented by the transition insertCard, it becomes active. While it is active transactions can occur (transition Transaction). At some time (after 0 or more transactions) the ATM will return to the idle state, ejecting the card as it does so (transition ejectCard). The model is accurate but it leaves out many details.

Return to the package diagram, select the machine, ATM_M, and click on "Make a refinement of this Machine..." Name the refinement ATM_R.

Open the class diagram of ATM_R and you will find a 'refined state machine' which is a clone of atm_sm. Open the state machine. Notice that the transitions refine their counterparts in the abstract level. At the moment the refinement is valid because it is an exact copy, but it doesn't make any progress. We will make the refinement more interesting by modifying the state machine and introducing more detail. The detail that we will introduce is that an ATM active session can result in ejecting the card with cash or without cash. We will also introduce some details of the process involved in a transaction. Firstly, we need to split the transition, ejectCard into two transitions representing the two outcomes.

a) Change the name of the transition ejectCard to ejectCardWithCash by selecting the transition and editing its name in the properties view.
b) Draw a new transition from state active to state idle.
c) With the new transition still selected, enter ejectCardWithoutCash as its name in the properties view.
d) Using the 'Add Refined Event/Transition' button in the 'Refines' tab of the properties view, add ejectCard as a refined transition.

The refined state machine should now look something like the one below. This screen-shot shows step d) where the event refinement relationship is being set.

Now we need to add some detail to show when each of these two eject card options are taken. We do this by adding a nested statemachine in the next step.

a) Using the 'State Features-Statemachine' palette option, add a nested state machine called active_sm to the state, active. 
b) In the properties view for the new state machine, set the translation kind to state sets.
c) Open the new state machine's diagram by right-clicking on it and selecting 'open diagram'.
d) Draw the state machine states, initial state and final states shown in the model below. (The transitions are discussed in the next step)

Notice that many of the transitions have the same name as transitions in the parent state machine. These transitions do not represent new events. Instead, they contribute more information about the transitions that have already been introduced to this refinement by the parent state machine. This is specified in the state machine model by an 'elaborates' property on the transition. The elaborates property forces the name of the elaborating transition to match that of the transition it elaborates. The transition must match the entry/exit characteristics of the parent transition it elaborates. For example, a transition that enters the parent state can only be elaborated by a transition from an initial state, an exit transition can only be elaborated by a transition to a final state and a self-loop transition can only be elaborated by a transition between states that are neither initial nor final. (In the last case the elaborating transition can either be another self-loop on one of the nested states, or it can be a transition between two different nested states). These well-formedness criteria are enforced by validation checks built into the drawing tool.

a) Draw a transition from the initial state to state awaitingPin.
b) Do not name it but instead select the transition called insertCard from the combo box on its properties view. Its name should automatically become the same as the transition it elaborates.
c) Repeat this process for the transitions ejectCardWithoutCash, Transaction and ejectCardWithCash, making sure they elaborate the transition with the same name from the parent.
      (Notice that each parent transition can only be elaborated once).
d) The transition pinEntered is a new transition and does not elaborate anything. Instead, enter its name using the name property text box.

This completes the tutorial. The model should prove all the POs automatically. Examine the generated Event-B machines to see how the model is translated.