State machine synthesis

UCEd implements an algorithm for the generation of a state machine from use cases. The principle of the state machine generation algorithm is as follow. For each use case, we augment an initially empty state transition machine with states and transitions such that each scenario in the use case is included as state transition sequences in the state transition machine. We use the operations effects (added and withdrawn conditions) to determine states.

Suppose ``-'' is an operator such that $C_{1}$ and $C_{2}$ being 2 sets of conditions, $C_{1} - C_{2}$ is a set obtained by removing all the conditions in $C_{2}$ from $C_{1}$, and $C_{1} + C_{2}$ is a set obtained by adding all the conditions in $C_{2}$ to $C_{1}$. Given a state s such that cond(s) are the characteristic conditions of s, the execution of operation op with added-condition add_conds(op) and withdrawn conditions withdr_conds(op) produces a state $s^{\prime}$ such that
cond($s^{\prime}$) = (cond(s) - withdr_conds(op)) + add_conds(op).

The finite state machine generation algorithm augments a state model with a use case as follow.

• First we determine a set of states corresponding to the use case preconditions.
• Then, starting from these first states, we follow each scenario by adding transitions corresponding to operations.
• After each transition, the resulting state is used as a starting point for the following operation in a scenario.
• Timeout triggered transitions are created to account for delays.

The state model has been generated from use case Log in. State 1 set of characteristic conditions is the use case set of preconditions {``PMSystem is ON''}. State 2 is obtained by considering the use case step 1. This state is characterized by the set of conditions {``System is ON'', ``Card is inserted''} since the operation ``insert Card'' adds the condition ``Card is inserted'' according to the domain model. The algorithm generates state 3 when adding step 1 extension 1a. State 3 is a sub-state of state 2 because of 1a extension condition ``Card status is irregular''. State 3 characteristic conditions are {``PMSystem is ON'', ``Card is inserted'', ``Card is irregular''}. Transition 7 ---[TIMEOUT(Timer1:60.0 second)]--> 8 is an example of timeout-triggered transition. This transition is created to consider extension 2a after delay. Timer1 is considered to be set as the state 7 is entered. Therefore the timeout event is produced if more than 60.0 seconds passes while in that state.