{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T20:10:13Z","timestamp":1746303013263,"version":"3.40.4"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-014-0304-0","type":"journal-article","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T06:02:05Z","timestamp":1405058525000},"page":"79-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal probabilistic analysis of detection properties in wireless sensor networks"],"prefix":"10.1145","volume":"27","author":[{"given":"Maissa","family":"Elleuch","sequence":"first","affiliation":[{"name":"CES Laboratory, National School of Engineers of Sfax, Sfax University, Soukra Street, 3052, Sfax, Tunisia"},{"name":"Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve W., H3G 1M8, Montreal, QC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Abid","sequence":"additional","affiliation":[{"name":"CES Laboratory, National School of Engineers of Sfax, Sfax University, Soukra Street, 3052, Sfax, Tunisia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.283"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2004.06.007"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abrams Z Goel A Plotkin S. Set K-cover algorithms for energy efficient monitoring in wireless sensor networks. In: Proceedings of the 3rd international symposium on information processing in sensor networks ACM New York pp. 424\u2013432","DOI":"10.1145\/984622.984684"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bernardeschi C Masci P Pfeifer H (2008) Early prototyping of wireless sensor network algorithms in PVS. In: Computer safety reliability and security. LNCS 5219. Springer Berlin pp 346\u2013359","DOI":"10.1007\/978-3-540-87698-4_29"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bernardeschi C Masci P Pfeifer H (2009) Analysis of wireless sensor network protocols in dynamic scenarios. In: Stabilization safety and security of distributed systems LNCS 5873. Springer Berlin pp 105\u2013119","DOI":"10.1007\/978-3-642-05118-0_8"},{"volume-title":"Measure theory","year":"2006","author":"Bogachev VI","key":"e_1_2_1_2_8_2"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/332656"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Elleuch M Hasan O Tahar S Abid M (2011) Formal analysis of a scheduling algorithm for wireless sensor networks. In: Formal methods and software engineering LNCS 6991. Springer Berlin pp 388\u2013403","DOI":"10.1007\/978-3-642-24559-6_27"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Elleuch M Hasan O Tahar S Abid M (2013) Formal probabilistic analysis of a wireless sensor network for forest fire detection. In: Symbolic computation in software science EPTCS 122. Open Publishing Association pp 1\u20139","DOI":"10.4204\/EPTCS.122.1"},{"key":"e_1_2_1_2_12_2","unstructured":"Elleuch M (2013) Formalization of the detection properties of WSNs in HOL. HOL code. http:\/\/hvg.ece.concordia.ca\/projects\/prob-it\/wsn.php"},{"key":"e_1_2_1_2_13_2","unstructured":"Feller W (1968) An introduction to probability theory and its applications vol 1. Wiley New York"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Fehnker A Van Hoesel L Mader A (2007) Modelling and verification of the LMAC protocol for wireless sensor networks. In: Integrated formal methods LNCS 4591. Springer Berlin pp 253\u2013272","DOI":"10.1007\/978-3-540-73210-5_14"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Fruth M (2006) Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Proceedings of international symposium on leveraging applications of formal methods verification and validation. IEEE Computer Society New York pp 290\u2013297","DOI":"10.1109\/ISoLA.2006.34"},{"volume-title":"Introduction to HOL: a theorem proving environment for higher-order logic","year":"1993","author":"Gordon MJC","key":"e_1_2_1_2_16_2"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hasan O Abbasi N Akbarpour B Tahar S Akbarpour R (2009) Formal reasoning about expectation properties for continuous random variables. In: Formal methods LNCS 5850. Springer Berlin pp 435\u2013450","DOI":"10.1007\/978-3-642-05089-3_28"},{"key":"e_1_2_1_2_18_2","unstructured":"Hasan O (2008) Formal probabilistic analysis using theorem proving. PhD thesis Concordia Univ. Montreal"},{"volume-title":"Reformatting fighter tactics","year":"2001","author":"Hewish M","key":"e_1_2_1_2_19_2"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl J Heller A (2011) Three chapters of measure theory in Isabelle\/HOL. In: Interactive theorem proving LNCS 6898. Springer Berlin pp 135\u2013151","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"e_1_2_1_2_21_2","unstructured":"The HOL theorem prover. http:\/\/hol.sourceforge.net\/"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Hanna Y Rajan H Zhang W (2008) Slede: a domain-specific verification framework for sensor network security protocol implementations. In: Proceedings of conference on wireless network security. ACM New York pp 109\u2013118","DOI":"10.1145\/1352533.1352551"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Hasan O Tahar S (2007) Formalization of continuous probability distributions. In: Automated deduction LNCS 4603. Springer Berlin pp 3\u201318","DOI":"10.1007\/978-3-540-73595-3_2"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9113-6"},{"key":"e_1_2_1_2_25_2","unstructured":"Hurd J (2002) Formal verification of probabilistic algorithms. PhD thesis Univ. of Cambridge Cambridge"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Jain S Srivastava S (2007) A survey and classification of distributed scheduling algorithms for sensor networks. In: Proceedings of international conference on sensor technologies and applications. IEEE Computer Society New York pp 88\u201393","DOI":"10.1109\/SENSORCOMM.2007.4394903"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/T-WC.2008.070933"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Lester DR (2007) Topology in PVS: continuous mathematics with applications. In: Proceedings of the second workshop on automated formal methods. ACM New York pp 11\u201320","DOI":"10.1145\/1345169.1345171"},{"key":"e_1_2_1_2_29_2","unstructured":"Liu C (2004) Randomized scheduling algorithm for wireless sensor neworks. In: Project report of randomized algorithm. University of Victoria Victoria"},{"key":"e_1_2_1_2_30_2","unstructured":"Liu L (2013) Formalization of discrete-time markov chains in HOL. PhD thesis Concordia Univ. Montreal May 2013."},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2006.77"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"MacKay DJC (1998) Introduction to Monte Carlo methods. In: Proceedings of NATO advanced study institute on learning in graphical models. Kluwer Academic Publishers Dordrecht pp 175\u2013204","DOI":"10.1007\/978-94-011-5014-9_7"},{"key":"e_1_2_1_2_33_2","unstructured":"Mhamdi T (2012) Information-theoretic analysis using theorem proving. PhD thesis Concordia Univ. Montreal December 2012"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Mhamdi T Hasan O Tahar S (2010) On the formalization of the lebesgue integration theory in HOL. In: Interactive theorem proving LNCS 6172. Springer Berlin pp 387\u2013402","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Mhamdi T Hasan O Tahar S (2011) Formalization of entropy measures in HOL. In: Interactive theorem proving LNCS 6898. Springer Berlin pp 233\u2013248","DOI":"10.1007\/978-3-642-22863-6_18"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky P Thorvaldsen S (2007) Formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time maude. In: Formal methods for open object-based distributed systems LNCS 4468. Springer Berlin pp 122\u2013140","DOI":"10.1007\/978-3-540-72952-5_8"},{"key":"e_1_2_1_2_37_2","unstructured":"The PRISM model checker. http:\/\/www.prismmodelchecker.org\/"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Rutten J Kwaiatkowska M Normal G Parker D (2004) Mathematical techniques for analyzing concurrent and probabilisitc systems. In: CRM monograph series. American Mathematical Society Providence","DOI":"10.1090\/crmm\/023"},{"key":"e_1_2_1_2_39_2","unstructured":"The real-time tool. http:\/\/heim.ifi.uio.no\/peterol\/RealTimeMaude\/."},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2010.09.008"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.170"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2009.05.002"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Xiao Y Zhang Y Sun X Chen H (2007) Asymptotic coverage and detection in randomized scheduling algorithm in wireless sensor networks. In: Proceedings of international conference on communications. IEEE New York pp 3541\u20133545","DOI":"10.1109\/ICC.2007.585"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2008.04.002"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.5121\/ijwmn.2010.2211"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Zheng M Sun J Liu Y Dong JS Gu Y (2011) Towards a model checker for NesC and wireless sensor networks. In: Formal methods and software engineering LNCS 6991. Springer Berlin pp 372\u2013387","DOI":"10.1007\/978-3-642-24559-6_26"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0304-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0304-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0304-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T19:28:52Z","timestamp":1746300532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0304-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"alternative-id":["10.1007\/s00165-014-0304-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0304-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2015,1]]}}}