Skip to main content
Top

2019 | OriginalPaper | Chapter

Formal Modelling and Incremental Verification of the MQTT IoT Protocol

Authors : Alejandro Rodríguez, Lars Michael Kristensen, Adrian Rutle

Published in: Transactions on Petri Nets and Other Models of Concurrency XIV

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
2.
go back to reference Aziz, B.: A formal model and analysis of an IoT protocol. Ad Hoc Netw. 36, 49–57 (2016)CrossRef Aziz, B.: A formal model and analysis of an IoT protocol. Ad Hoc Netw. 36, 49–57 (2016)CrossRef
4.
go back to reference 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) 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)
6.
go back to reference 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)CrossRef 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)CrossRef
7.
go back to reference 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)CrossRef 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)CrossRef
9.
go back to reference 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)CrossRef 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)CrossRef
11.
go back to reference 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) 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)
12.
go back to reference Jensen, K., Kristensen, L.: Coloured Petri nets: a graphical language for modelling and validation of concurrent systems. Commun. ACM 58(6), 61–70 (2015)CrossRef Jensen, K., Kristensen, L.: Coloured Petri nets: a graphical language for modelling and validation of concurrent systems. Commun. ACM 58(6), 61–70 (2015)CrossRef
13.
go back to reference Mladenov, K.: Formal verification of the implementation of the MQTT protocol in IoT devices. Master thesis, University of Amsterdam (2017) Mladenov, K.: Formal verification of the implementation of the MQTT protocol in IoT devices. Master thesis, University of Amsterdam (2017)
16.
go back to reference 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) 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)
17.
go back to reference Wortmann, F., Flüchter, K.: Internet of things. Bus. Inf. Syst. Eng. 57(3), 221–224 (2015)CrossRef Wortmann, F., Flüchter, K.: Internet of things. Bus. Inf. Syst. Eng. 57(3), 221–224 (2015)CrossRef
18.
go back to reference Zanolin, L., Ghezzi, C., Baresi, L.: An approach to model and validate publish/subscribe architectures. Proc. SAVCBS 3, 35–41 (2003) Zanolin, L., Ghezzi, C., Baresi, L.: An approach to model and validate publish/subscribe architectures. Proc. SAVCBS 3, 35–41 (2003)
Metadata
Title
Formal Modelling and Incremental Verification of the MQTT IoT Protocol
Authors
Alejandro Rodríguez
Lars Michael Kristensen
Adrian Rutle
Copyright Year
2019
Publisher
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-60651-3_5

Premium Partner