Refinement of Statemachines: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Colin
imported>Colin
Line 6: Line 6:


[[Image:Atm1.jpg]]
[[Image:Atm1.jpg]]
Return to the package diagram, select the machine, ATM_M, and click on "Make a refinement of this Machine..."
[[Image:Atm2.jpg]]

Revision as of 23:19, 17 June 2009

Refinement of Statemachines

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.

create a machine called ATM_A, open its class diagram and then add a statemachine called atm_sm to the canvas. Open the state machine and draw the state machine shown in the diagram below.

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