## 4 A UPPAAL-Based Formal Methodology for the UEMS
### The Formal Specification and Verification of the Ulems
When the Sck is active, it would send a 'Ping_Req' message within each predefined time period, which the Gw acknowledges with a 'Ping_Resp' message immediately. If the Sck does not receive a 'Ping_Resp' message within a predefined latency time, it will go into lost state and try to reconnect the Gw. Figure 5: Timed automata model of connect message subscriber. Figure 6: Timed automata model of connect message publisher. The formal verifications of the time automata are illustrated in Table 4.  
(2) Measure behavior. Monitoring various signals of a physical device is imperative in CPS. The more timely and frequent the data publishing is, the more precise and synchronized the virtual mirror of physical processing established in the computing system is. The normal approach is to sample the signals equidistant in time which is called Riemann sampling. However, the communication network of UEMS is usually the resource limited and unstable WSNs. The gateway, which is the message transfer station between the cloud server and the intelligent terminals, bears considerable information throughput. It is crystal clear that an increase of the number of nodes and communication traffic will inevitably heavier the burden of the network and further cause the instability of the network. To improve data exchange efficiency, a data sampling and publishing mechanism based on Lebesgue sampling [22], which samples the system when the output has changed with a specified amount, is adopted in this paper. The hybrid model of the proposed data exchange mechanism is illustrated in Figure 7.  
Where \(t\) is current time and \(t^{\prime}\) is the time of last data publishing. \(W(x(t))\) denotes a vector of monitoring data types of device at time \(t\):  
\[W(t)=[s_{1}(t),s_{2}(t)\ldots s_{n}(t)] \tag{4}\]  
where \(s_{i}(t)\) denotes the value of the \(i\)th monitoring data types at time \(x(t)\). And \(\Delta\) is the vector of the predefined threshold of the monitoring data type:  
\[\Delta=[\delta_{s_{1}},\delta_{s_{2}},\ldots\delta_{s_{n}}] \tag{5}\]  
where \(\delta_{s_{i}}\) is the predefined threshold of the monitoring data type \(s_{i^{\prime}}\) (\(i=1,2,\ldots n\)). \begin{table}
\begin{tabular}{p{142.3 pt} p{142.3 pt} p{142.3 pt}} \hline \hline
**Formal Description** & **Informal Description** & **Result** \\ \hline E\textless{}Sck.ACTIVE & Verify if the terminal can eventually finish connection in some condition. & PASS \\ \hline A[]Sck.LOST imply isPingResp == false and tS \textgreater{} T\_out & Verify if the terminal gets into lost state when it does not receive a response of heartbeat within the prescribed time & PASS \\ \hline A[]Sck.ACTIVE imply (isConnected == true and isSubM == true and isSubC == true and isSubU == true and isRegM == true and isRegC == true) & Verify if the terminal finishes the connection in the condition of completing subscription and registration & PASS \\ \hline \hline \end{tabular}
\end{table} 
Table 4: The formal verifications of the connect behavior. Figure 7: The hybrid model of the proposed data exchange mechanism. For example, if the power, current and voltage of an electric heater are the three monitoring data types, \(W(t)\) could be defined as \([power(t),\ current(t),voltage(t)]\), which implies that \(s_{1}\) is power,\(s_{2}\) is current and \(s_{3}\) is voltage. The hybrid model has two states, 'Data Sampling' and 'Data Publishing'. 'Data Sampling' state only samples concerned data and does not publish them while 'Data Publishing' state delivers the sampled data to certain receiver such as gateway. These two states can be transformed into each other when certain condition is satisfied:  
1. If current state is 'Data Sampling', the state will transform into 'Data Publishing' when the deviation between current sampled value and the sampled value of last 'Data Publishing' of any monitoring data type is greater than the predefined threshold, that is, \(|s_{i}(t)-s_{i}(t^{\prime})|>\delta_{s_{i}}\), \(i=1,\ 2,\ 3\ldots n\). If the condition is not satisfied, 'Data Sampling' state will be maintained.