Name
Abstract | ||
|---|---|---|
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 paper, we overcome these limitations by using higher-order-logic theorem proving to formally analyze the detection properties of randomly-deployed WSNsusing the randomized scheduling of nodes. Based on the probability theory, available in the HOL theorem prover, we 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, we formally analyze the detection performance of a WSN deployed for border security monitoring. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/s00165-014-0304-0 | Formal Asp. Comput. |
Keywords | Field | DocType |
detection probability,detection delay,scheduling,theorem proving,wireless sensor networks,performance analysis | HOL,Key distribution in wireless sensor networks,Model checking,Computer science,Scheduling (computing),Automated theorem proving,Theoretical computer science,Probabilistic analysis of algorithms,Probabilistic logic,Wireless sensor network,Distributed computing | Journal |
Volume | Issue | ISSN |
27 | 1 | 1433-299X |
Citations | PageRank | References |
2 | 0.38 | 27 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maissa Elleuch | 1 | 14 | 3.00 |
| Osman Hasan | 2 | 401 | 60.79 |
| Sofiène Tahar | 3 | 915 | 110.41 |
| Mohamed Abid | 4 | 58 | 18.25 |