## 5 Experiments
### Test Results
#### 5.3.2 Property 2  
Every DATA packet will be retransmitted until one of the conditions has been satisfied: (i) up to a maximum of five times; or (ii) an ACK packet is received. This property can be differentiated into two situations, and by using the syntax and semantics we mentioned before, they are formalized as:  
(i) Up to a maximum of five times:  
\[ \begin{array}{l}\
eg\exists_{x}(repeat(x,\textbf{DATA})\rightarrow\exists_{ t<x}(repeat(t,\textbf{DATA}))\rightarrow\exists_{u<x}(repeat(u,\textbf{DATA}))\rightarrow\\ \exists_{v<x}(repeat(v,\textbf{DATA}))\rightarrow\exists_{w<x}(repeat(w, \textbf{DATA})))\end{array} \]  
where \(repeat(x,\textbf{DATA})\) is defined by:  
\[ \begin{array}{l}(request(x)\wedge x.type=\textbf{DATA}\rightarrow\exists_{ y<x}(request(y)\wedge y.type\\ =\textbf{DATA}\wedge x.dataSequenceNum=y.dataSequenceNum))\end{array} \]  
(ii) An ACK packet is received:  
\[ \begin{array}{l}\forall_{x}(repeat(x,\textbf{DATA})\rightarrow\\ \exists_{z>x}(responds(z,x)\wedge z.type=\textbf{ACK}))\end{array} \]  
Compared to Property 1, this property written in the new protocol requirements is far more complex. We test this property through the traces separately collected during two days. The results are shown in Tables 2 and 3. These tables include the results for traces collected from different nodes (101 to 110) and gateways (500, 501). \begin{table}
\begin{tabular}{c c c c c} \hline
**Traces** & **Total Messages** & **Pass** & **Fail** & **Inconclusive** \\ \hline
101 & 67,409 & 22,446 & 0 & 0 \\
102 & 95,206 & 29,552 & 0 & 0 \\
103 & 81,709 & 32,243 & 0 & 1 \\
104 & 84,590 & 29,128 & 0 & 0 \\
105 & 69,274 & 23,981 & 0 & 0 \\
106 & 70,113 & 23,983 & 0 & 0 \\
107 & 79,807 & 26,717 & 0 & 0 \\
108 & 78,483 & 29,330 & 0 & 1 \\
109 & 87,196 & 26,117 & 0 & 0 \\
110 & 62,235 & 19,837 & 0 & 0 \\ Gateway 500 & 60,805 & 17,639 & 0 & 1 \\ Gateway 501 & 52,444 & 14,659 & 0 & 0 \\ \hline \end{tabular}.  
\end{table} 
Table 2: Test results for Property 2 (Day 1). For better illustrating the results, the proportion of verdicts are also shown in Figures 2 and 3. As expected, most of the traces return 'pass' verdicts and no 'fail' is detected. However, several 'inconclusive' verdicts can be observed from 500, 103 and 108 in Table 2 and 102, 106 and 110 in Table 3.  
After the analysis of these verdicts through the collected traces, we find out that they are caused by the uncertain existence of 'ACK' packets. Indeed, according to the formalized formula, we search an 'ACK' before the received 'DATA' packet. Nevertheless, when the 'DATA' packet is received at the beginning of a trace, we cannot conclude whether there is an 'ACK' or not. As a result, our algorithm produces 'inconclusive' verdicts. \begin{table}
\begin{tabular}{c c c c c} \hline
**Traces** & **Total Messages** & **Pass** & **Fail** & **Inconclusive** \\ \hline
101 & 13,203 & 4228 & 0 & 0 \\
102 & 18,342 & 5496 & 0 & 1 \\
103 & 15,744 & 5939 & 0 & 0 \\
104 & 18,852 & 6685 & 0 & 0 \\
105 & 14,711 & 5809 & 0 & 0 \\
106 & 12,851 & 5811 & 0 & 1 \\
107 & 18,663 & 6613 & 0 & 0 \\
108 & 18,440 & 7310 & 0 & 0 \\
109 & 17,985 & 5377 & 0 & 0 \\
110 & 12,879 & 4125 & 0 & 1 \\ Gateway 500 & 11,770 & 3310 & 0 & 0 \\ Gateway 501 & 11,509 & 3230 & 0 & 0 \\ \hline \end{tabular}
\end{table} 
Table 3: Test results for Property 2 (Day 2). Figure 2: Test results for Property 2 (Day 1). Although few 'inconclusive' have been observed, we may notice that no 'fail' verdict is raised during the testing process. This shows that this functional tested property conforms to the requirements through these nodes during two days. Another discussion can also be opened about these 'inconclusive' verdicts. When testing a protocol, these kinds of verdicts could be compared to interference. The human testers have then to analyze in depth if they are not false positives/negatives or errors raised during the testing process. In our case here, these verdicts are detected on different nodes Day 1 and Day 2.