# An Enhanced Mechanism for Fault Tolerance in Agricultural Wireless Sensor Networks
## 5 Fault-Tolerant Scheme for WSN in Precision Agriculture
### Fault-Tolerant Clusters
#### 5.1.2 Fault-Tolerant CH
To enable observation of the fault tolerance behavior of the model (i.e., the backup component behavior), two clocks were used to schedule the failure of both BSs (i.e., the primary BS and backup BS) and CHs (i.e., the primary CH and backup CH). ### Verification of the Properties

In this part of the formal verification, a set of _safety_ and _liveness_ properties of the fault-tolerant WSN's formal model were tested. The set of properties are summarized in Table 1. TCTL formal temporal logic was used to specify the temporal properties. \begin{table}
\begin{tabular}{l l l} \hline \hline
**Type** & **TCTL queries** & **Description** \\ \hline \multirow{7}{*}{Safety} & A[] not deadlock & The WSN never reaches a deadlock state. \\ \cline{2-3}  & A\textless{}forall (iid\_c) not(PrimaryCH(i).Fail and BackupCH(j).Fail) & The primary CH and the backup CH never fail at the same time. \\ \cline{2-3}  & A\textless{}forall (iid\_c) not(PrimaryCH(j). Safe and BackupCH(j).Safe) & The primary CH and its backup are in mutual exclusion. \\ \cline{2-3}  & A\textless{}not(PrimaryBS.Failed and BackupBS.Failed) & The primary BS and the backup BS never fail at the same time. \\ \cline{2-3}  & A\textless{}(PrimaryBS.Safe imply BackupBS.Fail) and (PrimaryBS.Fail exclusion. \\ \cline{2-3}  & imply BackupBS.Safe) & The primary BS and its backup are operating in mutual exclusion. \\ \hline \hline \end{tabular}
\end{table} 
Table 1: _Safety_ and _liveness_ properties. Figure 12: Simulation environment of the fault-tolerant WSN model. The property verification results are shown in Figure 13. As shown in the figure, it is evident that all the requirements are satisfied by the model, indicating the effectiveness of the proposed fault-tolerant scheme in both failure detection and correction. ## 7 Complexity Estimation of the Fault-Tolerant WSN Model

After confirming the effectiveness of the proposed model by using UPPAAL formal verification, it is essential to estimate its complexity. ### Estimation of Message Density

Let us assume that the function \(f(\alpha,\beta)\) refers to the transmitted messages in the WSN. Then, \(f(\alpha,\beta)=1+2\alpha(1+\beta)\) (i.e., CH, sensor node) represents the transferred messages between the different components in the WSN. The set of transferred messages \begin{table}
\begin{tabular}{l l l} \hline \hline
**Type** & **TCTL queries** & **Description** \\ \hline \multirow{7}{*}{Liveness} & A\(<\)forall (i:id\_s) forall (:jid\_c) (SensorNode(i)). & The collected data sent by the sensor node are always received \\  & DataTransmission\_State imply (PrimaryCH(j).data\_reception or & by the primary CH or the backup CH. \\  & BackupCH(j).data\_recognition)) & \\ \cline{2-3}  & A\(<\)\(\sim\)forallall(:id\_c) (PrimaryCH(i).data\_transmission or & \\  & BackupCH(i).data\_transmission) imply (PrimaryBS.data\_reception & The aggregated data sent by the CH are always received by the \\  & or BackupBS.data\_reception) & primary or the backup BS. \\ \cline{2-3}  & E\(<\)\(\sim\)EndUser.Data\_reception & The WSN always offers data for the end user. \\ \cline{2-3}  & A\(<\)\(\sim\)forall (iid\_c) (:j\(\succeq\) 50 imply (PrimaryCH(i).Fail and & After energy depletion of the primary CH, the backup CH takes \\  & BackupCH(j).Safe)) & over the role. \\ \cline{2-3}  & A\(<\)\(\sim\) zz \(\succeq\) = 100 imply PrimaryBS.Fail and BackupBS.Safe & The backup BS completes the task after the energy depletion of \\  & A\(<\)\(\sim\)forall (iid\_c) (PrimaryCH(i).Fail imply BackupCH(i).Safe) and & There is always one CH in operation (i.e., the primary or \\  & BackupCH(i). Fail imply PrimaryCH(i).Safe) & backup CH) \\ \cline{2-3}  & A\(<\)\(\sim\)(PrimaryBS.Fail imply BackupBS.Safe) and (BackupBS.Fail & There is always one BS in service. \\ \cline{2-3}  & imply PrimaryBS.Safe) & \\ \hline \hline \end{tabular}
\end{table} 
Table 1: _Cont._

Figure 13: _Safety_ and _liveness_ verification of the fault-tolerant WSN’s formal model. is resumed in requests and data transactions.