# 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
The new Primary BS then sends a failure alert to the final user containing the failed Primary BS identity, for the purpose of repairing. The new Primary BS also broadcasts its identity over the WSN and then assumes the Primary BS's tasks. After fixing the issue, it takes over the role of the Backup BS. It should be reiterated here that it is also possible to use more than one Backup BSs. In fact, the Backup BS acts as an emergency

Figure 10: Fault-tolerant backup BS process. Figure 9: Fault-tolerant primary BS process. redundant device for the Primary station in the event of its failure or shutdown. Such redundancy ensures the continuity and operation of the system even if any issue arises with the Primary BS (for which it is incapable of functioning properly). Therefore, the Backup BS possesses all the necessary information and resources to perform the tasks assigned to the Primary BS to carry on with the operation whenever required. This contributes to achieving self-stability and efficiency of the system over time. These processes are summarized in Algorithm 4. ```
Input: Base Station process Output: Fault-tolerant Base Station
```
1. Primary Base station0
2. Initialize clock y = 0
3. For loop = 1 to m CH
4. Ify = time slotloopthen
5. Send data request to the Primary CH;
6. Receive aggregated data from the Primary CH;
7. save CH data in CH_Data_File;
8. End If
9. Ify >= CH_TimeOut and data not received from CH then
10. Threads CH ID in Failed_CH_file;
11. End If
12. End For
13. Send CH_Data_File and Failed_CH_file to the End user;
14. Send Checkpoint (DataFile, Failed_CH_file)to the Backup BS;
15. Ify = BS_Hearbeat_time then
16. Send \"I am alive\" to the Backup BS
17. End If
18. End Primary Base station0 ```

**Algorithm 4**Fault-tolerant Base Station protocol

## 6 Formal Verification of the Fault-Tolerant Model

In this section, we present our simulation and a formal verification using the UPPAAL model checker for our fault-tolerant WSN model intended for the agricultural field. The Uppaal-4.1.26 framework is considered a sophisticated tool for verifying timed system models [47]. The framework is based on the theory of timed automata but it has been extended to support features required by the real-time system and protocol verification community. The query language of UPPAAL that is used to specify properties (that are to be checked) is a subset of TCTL (Timed Computation Tree Logic). TCTL is a formal temporal logic used for specifying and verifying temporal properties in timed systems. In fact, the UPPAAL model checker can provide a formal verification of the _safety_ and _liveness_ properties. For the readers, it may be mentioned again here that the _safety_ property ensures that some undesirables scenarios are not reachable while the _liveness_ property guarantees that certain desirable states are eventually achieved. UPPAAL's model checking capabilities use formal methods to systematically explore the system state space and validate whether the system satisfies these _safety_ and _liveness_ requirements in order to ensure the correctness and fault tolerance of the WSN system. ### Formal Model

As shown in Figure 11, a set of timed automata were designed for each WSN component: (a) PrimaryCH (i.e., primary Cluster Head), (b) BackupCH (i.e., backup Cluster Head), (c) EndUser (i.e., the end user), (d) PrimaryBS (i.e., primary Base Station), (e) BackupBS (i.e., backup Base Station), (f) SensorNode (i.e., sensor node). Figure 11: (a) Primary CH; (b) backup CH; (c) end user; (d) primary BS; (e) backup BS; (f) sensor node. ### Simulation

After designing the set of fault-tolerant WSN components using real-time timed automata and programming the necessary variables, clocks, and synchronization channels, the model simulation was obtained, as shown in Figure 12.

Here, the WSN was composed of 1 primary BS, 1 backup BS, and 10 clusters. Each cluster is composed of 1 primary CH, 1 backup CH, and 10 sensor nodes.