## 4 A UPPAAL-Based Formal Methodology for the UEMS
### The Formal Specification and Verification of the Ulems  
(1) Connection behavior. In the MQTTSN-based UEMS, an intelligent terminal is regarded as a client and needs to setup a connection to a gateway before it can exchange information with that gateway. The procedure of setting up a connection with a gateway is illustrated in Figure 3, in which it is assumed that the client requests the gateway to prompt for the transfer of Will topic and Will message. This request is indicated by setting the Will flag of the CONNECT message. The terminal then sends these two pieces of information to the gateway upon receiving the corresponding request messages WILLTOPICREQ and WILLMSGREQ. The procedure is terminated with the ACK message of register 'U_' topic sent by the gateway. Table 3 introduces the meaning of topics in Figure 4. \begin{table}
\begin{tabular}{c c c} \hline \hline
**Classification** & **Formal Specification** & **Description** \\ \hline reachability & \(E\)\(<\)\(>\)\(f\) & There exists a path where \(f\) eventually holds. \\ \hline safety & \(A[]\)\(f\) & For all paths \(f\) always holds. \\  & \(E[]\)\(f\) & There exists a path where \(f\) always holds. \\ \hline  & \(A\)\(<\)\(>\)\(f\) & For all paths \(f\) will eventually hold. \\  & \(F\)\(\rightarrow\)\(h\) & Whenever \(f\) holds \(h\) will eventually hold. \\ \hline \hline \end{tabular}
\end{table} 
Table 2: The description of query language in UPPAAL. Figure 3: The path formulae of the query language in UPPAAL. It should be noted that the upper half part of Figure 4 is the standard connection procedure of MQTT-SN while the lower half part, which includes topic subscription of 'M', 'C' and 'U' and topic registration of 'M_', 'C_' and 'U_', is our originality. Those basic topics are based on the major behaviors of intelligent terminals in the UEMS, which have been mentioned in Section 3.3. The proposed basic topics could help topic-oriented MQTT-SN avoid hidden troubles such as topic explosion. The formal specification of connection behavior based on timed automata model is depicted as Figures 5 and 6 (where the subscriber is instantiated as Gw and the publisher is instantiated as Sck). \begin{table}
\begin{tabular}{c c} \hline \hline
**Topic** & **Description of Behavior** \\ \hline M & Measure request from gateway \\ C & Control request from gateway \\ U & Update request from gateway \\ M\_ & Measure result from terminal \\ C\_ & Control result from terminal \\ U\_ & Update result from terminal \\ \hline Broker &
\begin{tabular}{c} Wifi/fiber/4G \\ Connect request from client \\ \end{tabular} \\ \hline Will topic request \\ \hline Will topic response from client \\ \hline Will message request \\ \hline Will message response from client \\ \hline Connect ack \\ \hline Subscribe 'M’ topic for client \\ \hline Subscribe 'M’ topic ack \\ \hline Subscribe 'C' topic for client \\ \hline Subscribe 'C' topic ack \\ \hline Subscribe 'C' topic ack \\ \hline Subscribe 'C’ topic ack \\ \hline Subscribe 'C’ topic ack \\ \hline Subscribe 'C’ topic ack \\ \hline Subscribe 'C’ topic ack \\ \hline Register 'M\_’ topic ack \\ \hline Register 'C\_’ topic ack \\ \hline Register 'U\_’ topic ack \\ \hline Register 'U\_’ topic ack \\ \hline Register 'U\_’ topic ack \\ \hline Register 'U\_’ topic ack \\ \hline Register 'U\_’ topic ack \\ \hline \hline \end{tabular}
\end{table} 
Table 3: The subdivided behaviors of the UEMS. Figure 4: The connect procedure of the MQTTSN-based communication protocol. Figures 5 and 6 are formal specifications of Figure 4, i.e., the connection behavior of intelligent terminals. After sending connecting request, a Sck would successively subscribe the 'M' topic, subscribe the 'C' topic, subscribe the 'U' topic, register the 'M_' topic, register the 'C_' topic, and register the 'U_' topic to a Gw. Additionally, some other details are added into Figures 5 and 6 to make the behavior more realistic. For example, the ping mechanism is introduced.