## 4 A UPPAAL-Based Formal Methodology for the UEMS
### The Formal Specification and Verification of the Ulems
2. If current state is 'Data Publishing', the state will transform into 'Data Sampling' when the deviations between current sampled value and the sampled value of last 'Data Publishing' of all monitoring data types are no more than the predefined threshold, that is, \(|W(t)-W(t^{\prime})|\leq\Delta\). If the condition is not satisfied, 'Data Publishing' state will be maintained. Additionally, once the state is transformed into 'Data Publishing', \(t^{\prime}\) will be updated to be \(t\). Figure 8 illustrates the formal specification of the measure behavior based on the timed automata model (where the publisher is instantiated as Sck and the subscriber is instantiated as Gw). The Sck applies the above-mentioned data exchange mechanism to decide whether the sampled data should be published. Some other details are also introduced to make the behavior more realistic. For example, the Sck would resend the sampled data until it receives a 'PubAck_M_' message in the condition of QoS > 0. In addition, each measurement message has a time mark. When the Gw receives a measurement message, it will check the message's time mark with the last measurement message of the same Sck. If the former is less than the later, the message will be judged as invalid data. The formal verifications of the time automata are illustrated in Table 5.  
(3) Control behavior. The control messages have high priority and real-time requirements. The QoS of the message is always set 1 or 2, which ensures that the message arrives at the receiver at least one time. In addition, the receiver must respond with an ACK message. The formal specifications of the control behavior based on timed automata model are depicted as Figure 9 (where the publisher is instantiated as Gw and the subscriber is instantiated as Sck). Similar to measure behavior, the Gw would resend the control command until it receives a 'PubAck_C' message in the condition of QoS > 0. In the condition of QoS > 0, the response message of Sck should explicitly indicate the execution result of the control so that the Gw could know whether the control is successful. \begin{table}
\begin{tabular}{l l l} \hline \hline
**Formal Specification** & **Informal Description** & **Result** \\ \hline E\textless{}>Sck.PUB\_M\_ & Verify if the measure can be eventually & \\  & triggered in some condition. & \\ \hline A[]Sck.MONITORING imply isActive == & Verify if the terminal gets into monitoring & \\  & true and isEnableM == true & state in the condition that it finished & \\  & connection and measure function is enable. & \\ \hline A[]Sck.PUB\_M\_ imply isToPub == true and isSubM == true and isRegM == true & Verify if the terminal publishes measure & \\  & isSubM == true and isRegM == true & information when the sampling data breaks & \\  & the threshold. & \\ \hline Al[] Sck.PUB\_M\_FIN imply (M\_Info.QoS > 0 & \\  & and M\_Ack.RC == Accepted and & \\  & M\_Info.MsgId == M\_Ack.MsgId) or & Verify if the terminal finishes publish process & \\  & when QoS \(\leq\) 0 or receiving correct ACK & \\  & when QoS \(>\) 0. & \\ \hline \hline \end{tabular}
\end{table} 
Table 5: The formal verifications of the measure behavior. The formal verifications of the time automata are illustrated in Table 6.  
(4) Upgrade behavior. To further support scalability of intelligent terminals, remote firmware upgrade is implemented to expand and update the functions of modules or devices. Since the UEMS in this paper is based on ZigBee wireless network, which cannot transmit all upgrade data at one delivery, the upgrade file needs to be divided into block data of appropriate length to transmit. In addition, a greedy algorithm is adopted to generate the upgrade file according to