Refinement of Statemachines

Refinement of Statemachines

INCOMPLETE - UNDER CONSTRUCTION

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.

a)  Create a new UML-B project using the New-UML-B Project Wizard
b) Create a machine called ATM_A using the package diagram palette Machine tool
c) Open its class diagram by selecting the machine and then clicking the button in the properties view (or using the pop-up menu).
d) Add a statemachine called atm_sm to the canvas using the diagram palette Statemachine tool. 
c) 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 important 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 a valid refinement 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 or without cash. We will also start to 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. Change the name of the