Formal probabilistic analysis of detection properties in wireless sensor networks

Verfasser / Beitragende:
[Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid]
Ort, Verlag, Jahr:
2015
Enthalten in:
Formal Aspects of Computing, 27/1(2015-01-01), 79-102
Format:
Artikel (online)
ID: 605516146
LEADER caa a22 4500
001 605516146
003 CHVBK
005 20210128100712.0
007 cr unu---uuuuu
008 210128e20150101xx s 000 0 eng
024 7 0 |a 10.1007/s00165-014-0304-0  |2 doi 
035 |a (NATIONALLICENCE)springer-10.1007/s00165-014-0304-0 
245 0 0 |a Formal probabilistic analysis of detection properties in wireless sensor networks  |h [Elektronische Daten]  |c [Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid] 
520 3 |a 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 WSNs using 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. 
540 |a British Computer Society, 2014 
690 7 |a Theorem proving  |2 nationallicence 
690 7 |a Wireless sensor networks  |2 nationallicence 
690 7 |a Scheduling  |2 nationallicence 
690 7 |a Performance analysis  |2 nationallicence 
690 7 |a Detection probability  |2 nationallicence 
690 7 |a Detection delay  |2 nationallicence 
700 1 |a Elleuch  |D Maissa  |u CES Laboratory, National School of Engineers of Sfax, Sfax University, Soukra Street, 3052, Sfax, Tunisia  |4 aut 
700 1 |a Hasan  |D Osman  |u Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada  |4 aut 
700 1 |a Tahar  |D Sofiène  |u Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada  |4 aut 
700 1 |a Abid  |D Mohamed  |u CES Laboratory, National School of Engineers of Sfax, Sfax University, Soukra Street, 3052, Sfax, Tunisia  |4 aut 
773 0 |t Formal Aspects of Computing  |d Springer London  |g 27/1(2015-01-01), 79-102  |x 0934-5043  |q 27:1<79  |1 2015  |2 27  |o 165 
856 4 0 |u https://doi.org/10.1007/s00165-014-0304-0  |q text/html  |z Onlinezugriff via DOI 
898 |a BK010053  |b XK010053  |c XK010000 
900 7 |a Metadata rights reserved  |b Springer special CC-BY-NC licence  |2 nationallicence 
908 |D 1  |a research-article  |2 jats 
949 |B NATIONALLICENCE  |F NATIONALLICENCE  |b NL-springer 
950 |B NATIONALLICENCE  |P 856  |E 40  |u https://doi.org/10.1007/s00165-014-0304-0  |q text/html  |z Onlinezugriff via DOI 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Elleuch  |D Maissa  |u CES Laboratory, National School of Engineers of Sfax, Sfax University, Soukra Street, 3052, Sfax, Tunisia  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Hasan  |D Osman  |u Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Tahar  |D Sofiène  |u Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Abid  |D Mohamed  |u CES Laboratory, National School of Engineers of Sfax, Sfax University, Soukra Street, 3052, Sfax, Tunisia  |4 aut 
950 |B NATIONALLICENCE  |P 773  |E 0-  |t Formal Aspects of Computing  |d Springer London  |g 27/1(2015-01-01), 79-102  |x 0934-5043  |q 27:1<79  |1 2015  |2 27  |o 165