{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:17:22Z","timestamp":1759335442797,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-69483-2_16","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T11:34:48Z","timestamp":1508153688000},"page":"266-280","source":"Crossref","is-referenced-by-count":19,"title":["A Framework for Modeling and Verifying IoT Communication Protocols"],"prefix":"10.1007","author":[{"given":"Maithily","family":"Diwan","sequence":"first","affiliation":[]},{"given":"Meenakshi","family":"D\u2019Souza","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"key":"16_CR1","unstructured":"Event-B. http:\/\/www.Event-B.org\/"},{"key":"16_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11813040_16","volume-title":"FM 2006: Formal Methods","author":"N Evans","year":"2006","unstructured":"Evans, N., Butler, M.: A proposal for records in Event-B. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 221\u2013235. Springer, Heidelberg (2006). doi: 10.1007\/11813040_16"},{"key":"16_CR4","unstructured":"Rodin Tool. http:\/\/wiki.Event-B.org\/index.php\/Rodin_Platform"},{"key":"16_CR5","unstructured":"Rodin Hand Book. https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/pdf\/rodin-doc.pdf"},{"key":"16_CR6","unstructured":"ProB tool. https:\/\/www3.hhu.de\/stups\/prob\/index.php\/Main_Page"},{"key":"16_CR7","unstructured":"Gartner newsroom. http:\/\/www.gartner.com\/newsroom\/id\/3165317"},{"issue":"1","key":"16_CR8","first-page":"11","volume":"3","author":"V Karagiannis","year":"2015","unstructured":"Karagiannis, V., Chatzimisios, P., Vazquez-Gallego, F., Alonso-Zarate, J.: A survey on application layer protocols for the internet of things. Trans. IoT Cloud Comput. 3(1), 11\u20137 (2015)","journal-title":"Trans. IoT Cloud Comput."},{"key":"16_CR9","unstructured":"MQTT Ver. 3.1.1. http:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/os\/mqtt-v3.1.1-os.html"},{"key":"16_CR10","unstructured":"MQTT-SN Ver. 1.2. http:\/\/mqtt.org\/new\/wp-content\/uploads\/2009\/06\/MQTT-SN_spec_v1.2.pdf"},{"key":"16_CR11","unstructured":"The Constrained Application Protocol (CoAP) RFC7252. https:\/\/tools.ietf.org\/html\/rfc7252"},{"key":"16_CR12","unstructured":"Extensible Messaging and Presence Protocol (XMPP) Core RFC6120. http:\/\/xmpp.org\/rfcs\/rfc6120.html"},{"key":"16_CR13","unstructured":"Advanced Message Queuing Protocol ver. 1.0. http:\/\/docs.oasis-open.org\/amqp\/core\/v1.0\/amqp-core-complete-v1.0.pdf"},{"key":"16_CR14","unstructured":"Pascal, C., Renato, S.: Event-B model decomposition, DEPLOY Plenary Technical Workshop (2009)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-33826-7_6","volume-title":"Software Engineering and Formal Methods","author":"A Salehi Fathabadi","year":"2012","unstructured":"Salehi Fathabadi, A., Butler, M., Rezazadeh, A.: A systematic approach to atomicity decomposition in Event-B. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 78\u201393. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33826-7_6"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Aziz, B.: A formal model and analysis of the MQ telemetry transport protocol. In: Ninth International Conference, Availability, Reliability and Security (ARES), pp. 59\u201368. Fribourg (2014)","DOI":"10.1109\/ARES.2014.15"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Gawanmeh, A.: Embedding and verification of ZigBee protocol stack in Event-B. In: Procedia Computer Science, vol. 5, pp. 736\u2013741. ISSN 1877\u20130509 (2011)","DOI":"10.1016\/j.procs.2011.07.097"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Che, X., Maag, S.: A passive testing approach for protocols in Internet of Things. In: Green Computing and Communications (GreenCom), IEEE and Internet of Things (iThings\/CPSCom), IEEE International Conference on and IEEE Cyber, Physical and Social Computing, pp. 678\u2013684. IEEE Press (2013)","DOI":"10.1109\/GreenCom-iThings-CPSCom.2013.124"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Lee, S., Kim, H., Hong, D.K., Ju, H.: Correlation analysis of MQTT loss and delay according to QoS level. In: The International Conference on Information Networking(ICOIN), pp. 714\u2013717. IEEE (2013)","DOI":"10.1109\/ICOIN.2013.6496715"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Thangavel, D., Ma, X., Valera, A., Tan, H.X., Tan, C.K.: Performance evaluation of MQTT and CoAP via a common middleware. In: IEEE Ninth International Conference, Intelligent Sensors, Sensor Networks and Information Processing (ISSNIP), pp. 1\u20136. IEEE Press (2014)","DOI":"10.1109\/ISSNIP.2014.6827678"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T14:18:24Z","timestamp":1750947504000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}