Abstract
Machine to Machine (M2M) communication and Internet of Things (IoT) are becoming still more pervasive with the increase of communicating devices used in cyber-physical environments. A prominent approach to communication between distributed devices in highly dynamic IoT environments is the use of publish-subscribe protocols such as the Message Queuing Telemetry Transport (MQTT) protocol. MQTT is designed to be light-weight while still being resilient to connectivity loss and component failures. We have developed a Coloured Petri Net model of the MQTT protocol logic using CPN Tools. The model covers all three quality of service levels provided by MQTT (at most once, at least once, and exactly once). For the verification of the protocol model, we show how an incremental model checking approach can be used to reduce the effect of the state explosion problem. This is done by exploiting that the MQTT protocol operates in phases comprised of connect, subscribe, publish, unsubscribe, and disconnect.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Adamski, M.A., Karatkevich, A., Wegrzyn, M.: Design of Embedded Control Systems, vol. 267. Springer, Boston (2005). https://doi.org/10.1007/0-387-28327-7
Aziz, B.: A formal model and analysis of an IoT protocol. Ad Hoc Netw. 36, 49–57 (2016)
Banks, A., Gupta, R.: MQTT Version 3.1.1. OASIS Standard, 29 (2014). http://docs.oasis-open.org/mqtt/mqtt/v3.1.1/mqtt-v3.1.1.html
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–208. IEEE Computer Society (2007)
Billington, J., Diaz, M.: Application of Petri Nets to Communication Networks: Advances in Petri Nets, vol. 1605. Springer, Heidelberg (1999). https://doi.org/10.1007/BFb0097770
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–359 (2014)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)
Desel, J., Reisig, W., Rozenberg, G. (eds.): Lectures on Concurrency and Petri Nets, Advances in Petri Nets. LNCS, vol. 3018. Springer, Heidelberg (2004). https://doi.org/10.1007/b98282
Eugster, P.T., Felber, P.A., Guerraoui, R., Kermarrec, A.-M.: The many faces of publish/subscribe. ACM Comput. Surv. (CSUR) 35(2), 114–131 (2003)
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–180. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44829-2_11
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–221. IEEE (2017)
Jensen, K., Kristensen, L.: Coloured Petri nets: a graphical language for modelling and validation of concurrent systems. Commun. ACM 58(6), 61–70 (2015)
Mladenov, K.: Formal verification of the implementation of the MQTT protocol in IoT devices. Master thesis, University of Amsterdam (2017)
MQTT essentials part 3: Client, broker and connection establishment. https://www.hivemq.com/blog/mqtt-essentials-part2-publish-subscribe
Rodriguez, A., Kristensen, L.M., Rutle, A.: Complete CPN model of the MQTT Protocol. via Dropbox. http://www.goo.gl/6FPVUq
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–196 (2017)
Wortmann, F., Flüchter, K.: Internet of things. Bus. Inf. Syst. Eng. 57(3), 221–224 (2015)
Zanolin, L., Ghezzi, C., Baresi, L.: An approach to model and validate publish/subscribe architectures. Proc. SAVCBS 3, 35–41 (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer-Verlag GmbH Germany, part of Springer Nature
About this chapter
Cite this chapter
Rodríguez, A., Kristensen, L.M., Rutle, A. (2019). Formal Modelling and Incremental Verification of the MQTT IoT Protocol. In: Koutny, M., Pomello, L., Kristensen, L. (eds) Transactions on Petri Nets and Other Models of Concurrency XIV. Lecture Notes in Computer Science(), vol 11790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-60651-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-662-60651-3_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-60650-6
Online ISBN: 978-3-662-60651-3
eBook Packages: Computer ScienceComputer Science (R0)