In the context of Wireless Sensor Networks (WSNs), the ability to detect an intrusion event is the most desired characteristic. Due to the randomness in nodes scheduling algorithm and sensor deployment, probabilistic techniques are used to analyze the detection properties of WSNs. However, traditional probabilistic analysis techniques, such as simulation and model checking, do not ensure accurate results, which is a severe limitation considering the mission-critical nature of most of the WSNs. In this chapter, the authors overcome these limitations by using higher-order-logic theorem proving to formally analyze the detection properties of randomly deployed WSNs using the randomized scheduling of nodes. Based on the probability theory, described in Chapters 5, they first formally reason about the intrusion period of any occurring event. This characteristic is then built upon to develop the fundamental formalizations of the key detection metrics: the detection probability and the detection delay. For illustration purposes, the authors formally analyze the detection performance of a WSN deployed for border security monitoring.
Top14.1 Detection Of A Wireless Sensor Network
Wireless Sensor Networks (WSNs) guarantee a continuous and automated monitoring of a given field without any human presence. This distinguishing feature is attained trough deploying a collection of battery-powered and wirelessly-connected miniature devices over the area of interest. The main task of such devices is to take measurements of the surrounding environment, to a base station to perform a centralized decision mechanism. Nowadays, wireless sensor networks are extensively being deployed in a wide range of real-world applications, such as home automation, detection of natural disasters, biological attacks and military tracking.
Since nodes are usually stand-alone and battery powered, extending the network lifetime is very critical. Therefore, the k-set randomized nodes scheduling is commonly applied to preserve energy (Abrams, Goel, & Plotkin, 2004). The main idea of such approach is to randomly organize the nodes into alternatively working sub-networks. Hence, during a given time slot, only the nodes belonging to the current active sub-network are powered up and may report an occurring event while all the other nodes are inactive and thus contribute to the power saving of the overall system.
In general, a wireless sensor network is expected to always report occurring events at any point of the monitored area to a base station with a short delay. This feature determines the detection abilities of the whole network and is measured through two key performance attributes: the detection probability and the detection delay. More specifically, the detection probability is the probability of detecting an occurring event within the monitored area. Due to the randomness in the nodes scheduling approach coupled with the unpredictable deployment of sensors, the detection characteristic cannot be usually ensured. Indeed, there is a possibility that an occurring event may not be detected if there are no nodes deployed in its surrounding area or the deployed nodes are inactive, due to random scheduling. Such situations will also lead to an infinite detection delay which is not desired at all. However, in most WSN applications, the network has to react according to intrusions detection. For example, in a WSN deployed for forest fire detection, the outbreak of afire should be simultaneously reported with the highest probability and the minimum delay, in order to alert the user. Consequently, missing an intrusion event can be really disastrous in the context of mission-critical WSN applications. Thus, probabilistic techniques are used to judge the detection properties of WSNs with the goal to maximize the probability of detection and minimize the detection delay.
Traditionally, paper-and-pencil proof based probabilistic techniques have been used to analyze the performance of random scheduling for WSNs. Simulation, using the Monte Carlo method, is then used to validate the analytical results, which can be error-prone. Due to the inherent incompleteness of simulation coupled with the rounding errors of computer arithmetic, which is a serious limitation for mission-critical WSNs.
Formal methods (Lveczky & Thorvaldsen, 2007; Bernardeschi, Masci & Pfeifer, 2008; Hanna, Rajan, & Zhang, 2008; Bernardeschi, Masci & Pfeifer, 2009; Elleuch, Hasan, Tahar & Abid, 2011, Zheng, Sun, Liu, Dong & Gu, 2011; Elleuch, Hasan, Tahar & Abid, 2013) can overcome the limitations of simulation and have been used to validate a wide range of hardware and software systems. Such methods enhance the analysis reliability using rigorous mathematical techniques to model and verify the given system. Formal methods have also been explored for analyzing WSNs but most of the existing work is focused on analyzing their functional aspects only (Fehnker, Hoesel & Mader 2007). However, given the wide application of WSNs in safety and mission-critical domains, there is a dire need to accurately assess their performance as well. With this motivation, this chapter provides a formal approach for an accurate performance analysis of the probabilistic detection properties of WSNs using the k-set randomized scheduling.