## 4 A UPPAAL-Based Formal Methodology for the UEMS
### Tool  
As mentioned above, UPPAAL model-checker is a simulator available to perform the formal specification and verification of the real-time system. It provides timed finite automata as the timed input language, which is appropriate for the proposed time automata-based formal specification. In addition, UPPAAL achieves the formal specification and verification in a unique environment, without the need for translation between formalism from the simulation to the formal verification environments. Thus, possible mistakes in the analyses that may occur during the translation can be avoided. Consequently, UPPAAL model-checker is selected in this paper as the simulator for the formal specification and verification.  
To execute the formal verification, UPPAAL uses a simplified version of TCTL and applies BNF to describe query language \(\varphi\). The query language consists of path formulae and state formulae. State formulae describe individual states, whereas path formulae quantify overpaths or traces of the model. The formal expression of \(\varphi\) is:  
\[\begin{array}{l}\varphi::=A[][f|E<>f|E[|f|A<>f|f\to f\\ f::=a|-f|(f)|f\lor f|f\wedge f|f\to f\end{array} \tag{3}\]  
where \(f\) is the state formula that is a logical expression describing the nature of the system to be verified while \(a\) can be a clock variable, an integer variable, or a location in the timed automaton. Characters \(A\) and \(E\) are used to quantify the path, where the path is a state transition sequence of the system. \(A\) indicates that for a given property, all paths in the model are satisfied. \(E\) indicates that for a given property, at least one path in the model can be satisfied. \(<>\) and [] are used to quantify the status on the path. [] indicates that all states on the desired path can satisfy given properties while \(<\!\!>\) indicates that at least one state on the desired path can satisfy given properties. Figure 3 illustrates the path formula.  
Path formulae can be classified into reachability, safety, and liveness (As illustrated in Table 2). Reachability properties ask whether for a given \(\varphi\), there exists a path starting at the initial state, such that \(\varphi\) is eventually satisfied along that path. Reachability properties do not by themselves guarantee the correctness of the system, but they validate the basic behavior of the model. Safety properties ask whether a bad result will never happen, or an awaited result is invariantly true. Liveness properties are of the form \"an awaited result will eventually happen\". With this type of properties, response conditions can be verified as follows \"whenever \(\phi\) is satisfied, eventually \(\varphi\) will be satisfied\".  
In addition, UPPAAL supports urgent locations (marked as 'u') and committed locations (marked as 'c'). In the urgent locations, time may not progress, but interleavings with normal states are allowed. A committed location is more restrictive: delay is not allowed, and the committed location must be left in the successor state. The synchronization mechanism in UPPAAL is a hand-shaking synchronization: two processes take a transition at the same time in the synchronization channel _ch_, one will have a _cht_ and the other _ch?_  
For direct use in the UPPAAL model-checker, the formal specification and verification of the behaviors can be executed according to the following steps:  
1. Modeling timed automata of the intended behavior
2. Describing the intended behavior in natural language.
3. Formalizing the informal behavior by using a subset of TCTL.
4. Translating the behavior properties into the input language permitted by UPPAAL and executing the formal verification.