# A Method for Modeling and Testing Near-Real-Time System Scenarios
## 4 Modeling the System Scenarios with Finite-State Machines
### Transformation Rules of UML State Machines to Extended FSM  
After defining a model presenting the system dynamics in the form of sequence diagrams, the next step is to define the rules for transforming the UML model into the EFSM model. The rules will use the sequence diagram model as input and the EFSM model as output. For a state machine model in UML without orthogonal states, path coverage can be determined, where starting from the initial state, all possible transitions (paths) to the final states will be determined. However, there remains the problem of testing a UML state machine that does not match the FSM state machine. To check the correctness of path coverage, a sequence diagram should be designed for each state, showing the use of each function present in the UML machine state. Any UML sequence diagram can be converted to an EFSM machine, as shown in this section. An extended finite-state machine (EFSM) \(M\) is a 6-tuple \((S,s_{0},P_{I},P_{O},V,T)\) (see [PERSON] et al. [33]):  
\(S\): a finite set of states;  
\(s_{0}\in S\): an initial state;  
\(P_{I}\): a finite set of input parameters;  
\(P_{O}\): is a finite set of output parameters;  
\(V\): a finite set of internal variables;  
\(T\): a finite set of transitions. \(T\): \(SxP_{I}xG\to SxUxP_{O}\)  
Each transition \(t\in T\) in a 6-tuple, where elements of this tuple are a source state, a destination state, an input event modeling the interaction of the input event with a list of input parameters \(P_{I}\), a logical expression (guard condition \(G\)) expressed by variables from \(V,P_{I}\) and comparison operators, a function that updates variables of \(V\) and \(P_{O}\), and an output function used to modify values of parameters \(P_{O}\) or variables \(V\). The most important rules for model transformation are presented below according to [PERSON] et al. [15]. These rules were used for model transformation in this article. Rule 1--Sequence diagram  
The sequence diagram instance maps directly to the EFSM instance and is given the same name. Moreover, when the initial lifeline is found, the initial state \(s_{0}\) of the EFSM is created. Rule 2--Transition  
A new state is created for all occurrences of the message or operation and added to EFSM. A new transition is added that connects the new state to its predecessor within the EFSM model. If an operation returns an output value, an additional state is added for each possible output of that operation. Rule 3--Switching elements: \(alt\) and \(opt\)  
For all instances with the \(alt\) or \(opt\) operator in the sequence diagram in the EFSM, a new state and a new transition are created for each operand. New transitions connect the current state to new states. Rule 4--_loop_  
For all instances of a sequence diagram with a \(loop\) interaction operator, the response message must be defined as the last operand message. An example transformation of a sequence diagram model into an EFSM machine model is shown in Figure 6. Only one loop is visible, which concerns the selection of the next route point. Without this loop, the diagram presents a DAG graph in which minimum flow methods can be used to determine path coverage for algorithm testing purposes. The figure shows two branches of the tree that correspond to the two alt alternatives shown in Figure 5. In this sequence diagram, there is only one loop, which starts at the last vertex \(S7\) and goes to the first vertex \(S0\). This model allows skipping this loop because the logic of the algorithm is identical for each subsequent waypoint of the route. In such a case, EFSM can be treated as an acyclic graph, which greatly simplifies the process of proving the correctness of the algorithm. In the case of the presented model, the set of variables \(V\) includes the flight mode of the UAV flight computer. The input parameters of \(P_{l}\) are the set of flight parameters for the mode, such as the UAV speed or flight altitude. The output parameters of \(P_{O}\) are the set and possible flight parameters of the UAV flying in a specific flight mode.