{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:10:30Z","timestamp":1743027030534,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319539454"},{"type":"electronic","value":"9783319539461"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-53946-1_6","type":"book-chapter","created":{"date-parts":[[2017,2,15]],"date-time":"2017-02-15T07:42:51Z","timestamp":1487144571000},"page":"93-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications"],"prefix":"10.1007","author":[{"given":"Maissa","family":"Elleuch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Abid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"issue":"6","key":"6_CR1","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1016\/j.compenvurbsys.2012.03.002","volume":"36","author":"Y Aslan","year":"2012","unstructured":"Aslan, Y., Korpeoglu, I., Ulusoy, O.: A framework for use of wireless sensor networks in forest fire detection and monitoring. Comput. Environ. Urban Syst. 36(6), 614\u2013625 (2012)","journal-title":"Comput. Environ. Urban Syst."},{"key":"6_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Miller, A.: Model checking medium access control for sensor networks. In: Proceedings of the 2nd Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 255\u2013262. IEEE Computer Society (2006)","DOI":"10.1109\/ISoLA.2006.16"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-05118-0_8","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"C Bernardeschi","year":"2009","unstructured":"Bernardeschi, C., Masci, P., Pfeifer, H.: Analysis of wireless sensor network protocols in dynamic scenarios. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 105\u2013119. Springer, Heidelberg (2009). doi:\n                    10.1007\/978-3-642-05118-0_8"},{"key":"6_CR5","unstructured":"Elleuch, M.: Formalization of the coverage properties of WSNs in HOL (2015). \n                    http:\/\/hvg.ece.concordia.ca\/projects\/prob-it\/wsn.php"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-24559-6_27","volume-title":"Formal Methods and Software Engineering","author":"M Elleuch","year":"2011","unstructured":"Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal analysis of a scheduling algorithm for wireless sensor networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 388\u2013403. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-24559-6_27"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal probabilistic analysis of a wireless sensor network for forest fire detection. In: Symbolic Computation in Software Science, Electronic Proceedings in Theoretical Computer Science, vol. 122, pp. 1\u20139. Open Publishing Association (2013)","DOI":"10.4204\/EPTCS.122.1"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Towards the formal performance analysis of wireless sensor networks. In: Proceedings of the 22nd Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, pp. 365\u2013370. IEEE Computer Society (2013)","DOI":"10.1109\/WETICE.2013.68"},{"issue":"1","key":"6_CR9","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s00165-014-0304-0","volume":"27","author":"M Elleuch","year":"2015","unstructured":"Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Formal probabilistic analysis of detection properties in wireless sensor networks. Formal Aspects Comput. 27(1), 79\u2013102 (2015)","journal-title":"Formal Aspects Comput."},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00867-2_1","volume-title":"Methods, Models and Tools for Fault Tolerance","author":"A Fehnker","year":"2009","unstructured":"Fehnker, A., Fruth, M., McIver, A.K.: Graphical modelling for simulation and formal analysis of wireless network protocols. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 1\u201324. Springer, Heidelberg (2009). doi:\n                    10.1007\/978-3-642-00867-2_1"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Fruth, M.: Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Proceedings of the 2nd Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 290\u2013297. IEEE Computer Society (2006)","DOI":"10.1109\/ISoLA.2006.34"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1002\/2014EA000044","volume":"2","author":"J Hart","year":"2015","unstructured":"Hart, J., Martinez, K.: Towards an environmental Internet of Things [IoT]. Earth Space Sci. 2, 1\u20137 (2015)","journal-title":"Earth Space Sci."},{"key":"6_CR13","unstructured":"Hasan, O.: Formal probabilistic analysis using theorem proving. Ph.D. thesis, Concordia University, Montreal, QC, Canada (2008)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-73595-3_2","volume-title":"Automated Deduction \u2013 CADE-21","author":"O Hasan","year":"2007","unstructured":"Hasan, O., Tahar, S.: Formalization of continuous probability distributions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 3\u201318. Springer, Heidelberg (2007). doi:\n                    10.1007\/978-3-540-73595-3_2"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-22863-6_12"},{"key":"6_CR16","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge, Cambridge, UK (2002)"},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/JETCAS.2013.2244771","volume":"3","author":"M Lazarescu","year":"2013","unstructured":"Lazarescu, M.: Design of a WSN platform for long-term environmental monitoring for IoT applications. IEEE J. Emerg. Sel. Topics Circ. Syst. 3(1), 1\u20136 (2013)","journal-title":"IEEE J. Emerg. Sel. Topics Circ. Syst."},{"issue":"6","key":"6_CR18","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1109\/TPDS.2006.77","volume":"17","author":"C Liu","year":"2006","unstructured":"Liu, C., Wu, K., Xiao, Y., Sun, B.: Random coverage with guaranteed connectivity: joint scheduling for wireless sensor networks. IEEE Trans. Parallel Distrib. Syst. 17(6), 562\u2013575 (2006)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"MacKay, D.: Introduction to Monte Carlo methods. In: Proceedings of NATO Advanced Study Institute on Learning in Graphical Models, pp. 175\u2013204. Kluwer Academic Publishers (1998)","DOI":"10.1007\/978-94-011-5014-9_7"},{"key":"6_CR20","unstructured":"Mainetti, L., Patrono, L., Vilei, A.: Evolution of wireless sensor networks towards the internet of things: a survey. In: Proceedings of the 19th International Conference on Software, Telecommunications and Computer Networks, pp. 1\u20136. IEEE (2011)"},{"key":"6_CR21","unstructured":"Mhamdi, T.: Information-theoretic analysis using theorem proving. Ph.D. thesis, Concordia University, Montreal, QC, Canada, December 2012"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-72952-5_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time Maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 122\u2013140. Springer, Heidelberg (2007). doi:\n                    10.1007\/978-3-540-72952-5_8"},{"key":"6_CR23","series-title":"CRM Monograph Series","doi-asserted-by":"crossref","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems","author":"J Rutten","year":"2004","unstructured":"Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series. American Mathematical Society, Providence (2004)"},{"issue":"2","key":"6_CR24","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10796-014-9489-2","volume":"17","author":"A Whitmore","year":"2015","unstructured":"Whitmore, A., Agarwal, A., Xu, L.: The internet of things-a survey of topics and trends. Inf. Syst. Front. 17(2), 261\u2013274 (2015)","journal-title":"Inf. Syst. Front."},{"issue":"6","key":"6_CR25","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1007\/s11036-005-4442-8","volume":"10","author":"K Wu","year":"2005","unstructured":"Wu, K., Gao, Y., Li, F., Xiao, Y.: Lightweight deployment-aware scheduling for wireless sensor networks. Mob. Netw. Appl. 10(6), 837\u2013852 (2005)","journal-title":"Mob. Netw. Appl."},{"issue":"4","key":"6_CR26","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1109\/TC.2009.170","volume":"59","author":"Y Xiao","year":"2010","unstructured":"Xiao, Y., Chen, H., Wu, K., Sun, B., Zhang, Y., Sun, X., Liu, C.: Coverage and detection of a randomized scheduling algorithm in wireless sensor networks. IEEE Trans. Comput. 59(4), 507\u2013521 (2010)","journal-title":"IEEE Trans. Comput."},{"issue":"7","key":"6_CR27","doi-asserted-by":"publisher","first-page":"964","DOI":"10.1002\/wcm.863","volume":"11","author":"Y Xiao","year":"2011","unstructured":"Xiao, Y., Zhang, Y.: Divide-and conquer-based surveillance framework using robots, sensor nodes, and RFID tags. Wirel. Commun. Mob. Comput. 11(7), 964\u2013979 (2011)","journal-title":"Wirel. Commun. Mob. Comput."},{"issue":"12","key":"6_CR28","doi-asserted-by":"publisher","first-page":"2292","DOI":"10.1016\/j.comnet.2008.04.002","volume":"52","author":"J Yick","year":"2008","unstructured":"Yick, J., Mukherjee, B., Ghosal, D.: Wireless sensor network survey. Comput. Netw. 52(12), 2292\u20132330 (2008)","journal-title":"Comput. Netw."},{"issue":"1","key":"6_CR29","doi-asserted-by":"publisher","first-page":"156","DOI":"10.5121\/ijwmn.2010.2211","volume":"12","author":"H Zayani","year":"2010","unstructured":"Zayani, H., Barkaoui, K., Ayed, R.B.: Probabilistic verification and evaluation of backoff procedure of the WSN ECo-MAC protocol. Int. J. Wirel. Mob. Netw. 12(1), 156\u2013170 (2010)","journal-title":"Int. J. Wirel. Mob. Netw."},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-24559-6_26","volume-title":"Formal Methods and Software Engineering","author":"M Zheng","year":"2011","unstructured":"Zheng, M., Sun, J., Liu, Y., Dong, J.S., Gu, Y.: Towards a model checker for NesC and wireless sensor networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 372\u2013387. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-24559-6_26"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53946-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T08:45:05Z","timestamp":1558514705000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53946-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319539454","9783319539461"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53946-1_6","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 February 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FTSCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Formal Techniques for Safety-Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ftscs2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ftscs.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}