{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:49:16Z","timestamp":1762876156333},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662606506"},{"type":"electronic","value":"9783662606513"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-662-60651-3_5","type":"book-chapter","created":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T01:04:25Z","timestamp":1574211865000},"page":"126-145","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Formal Modelling and Incremental Verification of the MQTT IoT Protocol"],"prefix":"10.1007","author":[{"given":"Alejandro","family":"Rodr\u00edguez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars Michael","family":"Kristensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrian","family":"Rutle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-28327-7","volume-title":"Design of Embedded Control Systems","author":"MA Adamski","year":"2005","unstructured":"Adamski, M.A., Karatkevich, A., Wegrzyn, M.: Design of Embedded Control Systems, vol. 267. Springer, Boston (2005). \nhttps:\/\/doi.org\/10.1007\/0-387-28327-7"},{"key":"5_CR2","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":"5_CR3","unstructured":"Banks, A., Gupta, R.: MQTT Version 3.1.1. OASIS Standard, 29 (2014). \nhttp:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/mqtt-v3.1.1.html"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Baresi, L., Ghezzi, C., Mottola, L.: On accurate automatic verification of publish-subscribe architectures. In: Proceedings of the 29th International Conference on Software Engineering, pp. 199\u2013208. IEEE Computer Society (2007)","DOI":"10.1109\/ICSE.2007.57"},{"key":"5_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097770","volume-title":"Application of Petri Nets to Communication Networks: Advances in Petri Nets","author":"J Billington","year":"1999","unstructured":"Billington, J., Diaz, M.: Application of Petri Nets to Communication Networks: Advances in Petri Nets, vol. 1605. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/BFb0097770"},{"issue":"4","key":"5_CR6","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1109\/JIOT.2014.2337336","volume":"1","author":"S Chen","year":"2014","unstructured":"Chen, S., Xu, H., Liu, D., Hu, B., Wang, H.: A vision of IoT: applications, challenges, and opportunities with China perspective. IEEE Internet Things J. 1(4), 349\u2013359 (2014)","journal-title":"IEEE Internet Things J."},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR8","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/b98282","volume-title":"Lectures on Concurrency and Petri Nets, Advances in Petri Nets","year":"2004","unstructured":"Desel, J., Reisig, W., Rozenberg, G. (eds.): Lectures on Concurrency and Petri Nets, Advances in Petri Nets. LNCS, vol. 3018. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/b98282"},{"issue":"2","key":"5_CR9","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/857076.857078","volume":"35","author":"PT Eugster","year":"2003","unstructured":"Eugster, P.T., Felber, P.A., Guerraoui, R., Kermarrec, A.-M.: The many faces of publish\/subscribe. ACM Comput. Surv. (CSUR) 35(2), 114\u2013131 (2003)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-44829-2_11","volume-title":"Model Checking Software","author":"D Garlan","year":"2003","unstructured":"Garlan, D., Khersonsky, S., Kim, J.S.: Model checking publish-subscribe systems. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 166\u2013180. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-44829-2_11"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Houimli, M., Kahloul, L., Benaoun, S.: Formal specification, verification and evaluation of the MQTT protocol in the Internet of Things. In: Mathematics and Information Technology, pp. 214\u2013221. IEEE (2017)","DOI":"10.1109\/MATHIT.2017.8259720"},{"issue":"6","key":"5_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/2663340","volume":"58","author":"K Jensen","year":"2015","unstructured":"Jensen, K., Kristensen, L.: Coloured Petri nets: a graphical language for modelling and validation of concurrent systems. Commun. ACM 58(6), 61\u201370 (2015)","journal-title":"Commun. ACM"},{"key":"5_CR13","unstructured":"Mladenov, K.: Formal verification of the implementation of the MQTT protocol in IoT devices. Master thesis, University of Amsterdam (2017)"},{"key":"5_CR14","unstructured":"MQTT essentials part 3: Client, broker and connection establishment. \nhttps:\/\/www.hivemq.com\/blog\/mqtt-essentials-part2-publish-subscribe"},{"key":"5_CR15","unstructured":"Rodriguez, A., Kristensen, L.M., Rutle, A.: Complete CPN model of the MQTT Protocol. via Dropbox. \nhttp:\/\/www.goo.gl\/6FPVUq"},{"key":"5_CR16","unstructured":"Wang, R., Kristensen, L., Meling, H., Stolz, V.: Application of model-based testing on a quorum-based distributed storage. In: Proceedings of PNSE 2017, volume 1846 of CEUR Workshop Proceedings, pp. 177\u2013196 (2017)"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s12599-015-0383-3","volume":"57","author":"F Wortmann","year":"2015","unstructured":"Wortmann, F., Fl\u00fcchter, K.: Internet of things. Bus. Inf. Syst. Eng. 57(3), 221\u2013224 (2015)","journal-title":"Bus. Inf. Syst. Eng."},{"key":"5_CR18","first-page":"35","volume":"3","author":"L Zanolin","year":"2003","unstructured":"Zanolin, L., Ghezzi, C., Baresi, L.: An approach to model and validate publish\/subscribe architectures. Proc. SAVCBS 3, 35\u201341 (2003)","journal-title":"Proc. SAVCBS"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency XIV"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-60651-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T01:10:29Z","timestamp":1574212229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-60651-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783662606506","9783662606513"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-60651-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}