ATM Example

ATM Example

This part should help to give you a first taste of using PAT to analyze UML state machines by leading you through a simple example which is picked from [UMLGuide] and included in PAT.

The input is a UML specification which has been formatted using the XML Metadata Interchange (XMI) syntax, which is the
Object Management Group standard of exchanging UML diagrams. From this input, a corresponding CSP# specification is automatically generated. The following is the basic description of a simplified ATM system as the following figure shows. This system might be in one of three basic states: Idle (waiting for customer interaction), Active (handling a customer's transaction), and Maintenance (perhaps having its cash store replenished). While Active, the behavior of the ATM follows a simple path: Validate the customer, select a transaction, process the transaction, and then print a receipt. After printing, the ATM returns to the Idle state. These stages of behavior are represented as the states Validating, Selecting, Processing, and Printing.

In order to analyze the above UML state machine into CSP#, you may click "Import" in the "File" menu to include its XMI file. Then you will get the translated CSP# model as the following shows:

//====================Global Variable Definitions====================
var more = false;
//====================Process Definitions====================

System()= StateMachine_0();

StateMachine_0()= Initial_0();

Initial_0()= (From_Initial_0_to_Idle_Transition_0->Idle());

Idle()= ((cardInserted->Active(0))[](maintain->Maintenance()));

Maintenance()= (finish->Idle());

Active(i)= (readCard->ActiveRegion_0(i));

ActiveRegion_0(i)= case { (i == 1):Validating() (i == 2):Selecting() (i == 3):Processing() (i == 4):Printing() true:Initial_1()};

Initial_1()= (From_Initial_0_to_Validating_Transition_0->Validating());

Validating()= (From_Validating_to_Selecting_Transition_0->Selecting());

Selecting()= (From_Selecting_to_Processing_Transition_0->Processing());

Processing()=((From_Processing_to_Selecting_Transition_0->([more]Selecting()))[] (From_Processing_to_Printing_Transition_0->Printing()));

Printing()= atomic{(From_Printing_to_Idle_Transition_0-> atomic{(ejectCard->Skip)}; Idle())};

Interested readers can refer to [ZHANGL10] for the detailed translation schemes. After finishing importing, the user can use the simulation and verification functions for CSP# models to analyze and verify state machines.