{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:28:53Z","timestamp":1778498933574,"version":"3.51.4"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031162091","type":"print"},{"value":"9783031162107","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-16210-7_43","type":"book-chapter","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T23:03:09Z","timestamp":1663714989000},"page":"528-541","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Formal Verification Model for\u00a0IoT Based Applications Using Event-B"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2540-1890","authenticated-orcid":false,"given":"Rihab","family":"Omri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3867-4441","authenticated-orcid":false,"given":"Zinah Hussein","family":"Toman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1920-1825","authenticated-orcid":false,"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,9,21]]},"reference":[{"key":"43_CR1","doi-asserted-by":"crossref","unstructured":"Al-Qaseemi, S.A., Almulhim, H.A., Almulhim, M.F., Chaudhry, S.R.: IoT architecture challenges and issues: lack of standardization. In: 2016 Future Technologies Conference (FTC), pp. 731\u2013738. IEEE (2016)","DOI":"10.1109\/FTC.2016.7821686"},{"issue":"2","key":"43_CR2","doi-asserted-by":"publisher","first-page":"1561","DOI":"10.1109\/COMST.2018.2877382","volume":"21","author":"W Ayoub","year":"2018","unstructured":"Ayoub, W., Samhat, A.E., Nouvel, F., Mroue, M., Pr\u00e9votet, J.C.: Internet of mobile things: LoRaWAN, DASH7, and NB-IoT in LPWANs standards and supported mobility. IEEE Commun. Surv. Tutorials 21(2), 1561\u20131581 (2018)","journal-title":"IEEE Commun. Surv. Tutorials"},{"key":"43_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.adhoc.2015.05.013","volume":"36","author":"B Aziz","year":"2016","unstructured":"Aziz, B.: A formal model and analysis of an IoT protocol. Ad Hoc Netw. 36, 49\u201357 (2016)","journal-title":"Ad Hoc Netw."},{"key":"43_CR4","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-74107-7_3","volume-title":"Logics of Specification Languages","author":"D Cansell","year":"2008","unstructured":"Cansell, D., M\u00e9ry, D.: The event-B modelling method: concepts and case studies. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of Specification Languages. MTCSAES, pp. 47\u2013152. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74107-7_3"},{"issue":"4","key":"43_CR5","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/s11704-015-4362-0","volume":"9","author":"X Chen","year":"2015","unstructured":"Chen, X., Li, A., Zeng, X., Guo, W., Huang, G.: Runtime model based approach to IoT application development. Front. Comp. Sci. 9(4), 540\u2013553 (2015)","journal-title":"Front. Comp. Sci."},{"key":"43_CR6","series-title":"Studies in Computational Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-48829-5_7","volume-title":"Intelligent Distributed Computing X","author":"F Ciccozzi","year":"2017","unstructured":"Ciccozzi, F., Spalazzese, R.: MDE4IoT: supporting the internet of things with model-driven engineering. In: IDC 2016. SCI, vol. 678, pp. 67\u201376. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-48829-5_7"},{"key":"43_CR7","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/j.comnet.2018.11.017","volume":"148","author":"M Eldefrawy","year":"2019","unstructured":"Eldefrawy, M., Butun, I., Pereira, N., Gidlund, M.: Formal security analysis of lorawan. Comput. Netw. 148, 328\u2013339 (2019)","journal-title":"Comput. Netw."},{"key":"43_CR8","doi-asserted-by":"crossref","unstructured":"Elhadi, S., Marzak, A., Sael, N.: Operating models of network protocols IoT: short-range protocols. In: 2020 International Symposium on Advanced Electrical and Communication Technologies (ISAECT), pp. 1\u20136. IEEE (2020)","DOI":"10.1109\/ISAECT50560.2020.9523646"},{"key":"43_CR9","unstructured":"Elsayed, E.K., Diab, L., Ibrahim, A.A.: Formal verification of an efficient architecture to enhance the security in IoT"},{"issue":"10","key":"43_CR10","doi-asserted-by":"publisher","first-page":"216","DOI":"10.3390\/fi11100216","volume":"11","author":"MA Ert\u00fcrk","year":"2019","unstructured":"Ert\u00fcrk, M.A., Ayd\u0131n, M.A., B\u00fcy\u00fckakka\u015flar, M.T., Evirgen, H.: A survey on lorawan architecture, protocol and technologies. Future Internet 11(10), 216 (2019)","journal-title":"Future Internet"},{"key":"43_CR11","doi-asserted-by":"publisher","first-page":"736","DOI":"10.1016\/j.procs.2011.07.097","volume":"5","author":"A Gawanmeh","year":"2011","unstructured":"Gawanmeh, A.: Embedding and verification of zigbee protocol stack in event-b. Procedia Comput. Sci. 5, 736\u2013741 (2011)","journal-title":"Procedia Comput. Sci."},{"key":"43_CR12","doi-asserted-by":"crossref","unstructured":"Jarrar, A., Gadi, T., Balouki, Y.: Modeling the internet of things system using complex adaptive system concepts. In: Proceedings of the 2nd International Conference on Computing and Wireless Communication Systems, pp. 1\u20136 (2017)","DOI":"10.1145\/3167486.3167508"},{"key":"43_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-030-00856-7_25","volume-title":"Model and Data Engineering","author":"S Marir","year":"2018","unstructured":"Marir, S., Belala, F., Hameurlain, N.: A formal model for interaction specification and analysis in IoT applications. In: Abdelwahed, E.H., Bellatreche, L., Golfarelli, M., M\u00e9ry, D., Ordonez, C. (eds.) MEDI 2018. LNCS, vol. 11163, pp. 371\u2013384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00856-7_25"},{"issue":"4","key":"43_CR14","doi-asserted-by":"publisher","first-page":"2109","DOI":"10.1007\/s11277-019-06832-x","volume":"110","author":"S Naoui","year":"2020","unstructured":"Naoui, S., Elhdhili, M.E., Azouz Saidane, L.: Novel enhanced lorawan framework for smart home remote control security. Wireless Pers. Commun. 110(4), 2109\u20132130 (2020)","journal-title":"Wireless Pers. Commun."},{"key":"43_CR15","doi-asserted-by":"crossref","unstructured":"Navani, D., Jain, S., Nehra, M.S.: The internet of things (IoT): a study of architectural elements. In: 2017 13th International Conference on Signal-Image Technology & Internet-Based Systems (SITIS), pp. 473\u2013478. IEEE (2017)","DOI":"10.1109\/SITIS.2017.83"},{"key":"43_CR16","doi-asserted-by":"crossref","unstructured":"Pek, E., Bogunovic, N.: Formal verification of logical link control and adaptation protocol. In: Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No. 04CH37521), vol. 2, pp. 583\u2013586. IEEE (2004)","DOI":"10.1109\/MELCON.2004.1346997"},{"key":"43_CR17","doi-asserted-by":"crossref","unstructured":"Sharma, C., Gondhi, N.K.: Communication protocol stack for constrained IoT systems. In: 2018 3rd International Conference on Internet of Things: Smart Innovation and Usages (IoT-SIU), pp. 1\u20136. IEEE (2018)","DOI":"10.1109\/IoT-SIU.2018.8519904"},{"key":"43_CR18","unstructured":"Vermesan, O., Friess, P.: Internet of things: converging technologies for smart environments and integrated ecosystems. River publishers (2013)"},{"issue":"6","key":"43_CR19","doi-asserted-by":"publisher","first-page":"1888","DOI":"10.3390\/s18061888","volume":"18","author":"I You","year":"2018","unstructured":"You, I., Kwon, S., Choudhary, G., Sharma, V., Seo, J.T.: An enhanced lorawan security protocol for privacy preservation in IoT with a case study on a smart factory-enabled parking system. Sensors 18(6), 1888 (2018)","journal-title":"Sensors"}],"container-title":["Communications in Computer and Information Science","Advances in Computational Collective Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-16210-7_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,4]],"date-time":"2024-10-04T06:07:33Z","timestamp":1728022053000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-16210-7_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031162091","9783031162107"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-16210-7_43","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"21 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}