Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Wireless Personal Communications
Erschienen in: Wireless Personal Communications 2/2021

26.02.2021

Formal Specification and Verification of MQTT Protocol in PlusCal-2

verfasst von: Sabina Akhtar, Ehtesham Zahoor

Erschienen in: Wireless Personal Communications | Ausgabe 2/2021

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The recent rise in adaptation of Internet of Things (IoT) concepts has potential to transform industries such as healthcare, manufacturing and power-grids. The communication protocols are at the heart of IoT and one such lightweight protocol being in widespread use is the Message Queue Telemetry Transport (MQTT) protocol. In this paper, we address the need to verify the correctness of the MQTT protocol. We have proposed a PlusCal-2 and TLA+ based formal model to both model check the safety and liveness properties and provide execution traces in case of any violation. We have detailed our models and provided performance analysis results to explain the practicality of our technique.
Vorheriger Artikel A Novel Encryption Approach Based on Vigenère Cipher for Secure Data Communication
Nächster Artikel Folded Substrate Integrated Waveguide Based Multiband Filter for Wi-Fi6E Application

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
Literatur
1.
Houimli, M., Kahloul, L., & Benaoun, S.: Formal specification, verification and evaluation of the MQTT protocol in the Internet of Things. pp. 214–221 (2017)
2.
Vinoski, S. (2006). Advanced message queuing protocol. IEEE Internet Computing, 10(6), 87–89.CrossRef
3.
4.
Banks, A., & Gupta, R. (29 October 2014). MQTT version 3.1.1.
5.
Kovatsch, M. (2013). CoAP for the web of things: From tiny resource-constrained devices to the web browser. In: Proceedings of the 2013 ACM Conference on Pervasive and Ubiquitous Computing Adjunct Publication. UbiComp ’13 Adjunct (pp. 1495–1504). New York, NY: ACM. https://​doi.​org/​10.​1145/​2494091.​2497583.
6.
Karagiannis, V., Chatzimisios, P., Vázquez-Gallego, F., & Alonso-Zarate, J. (2015). A survey on application layer protocols for the internet of things. Transaction on IoT and Cloud Computing, 3, 11–17.
7.
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., & Deardeuff, M. (2015). How amazon web services uses formal methods. Communications of the ACM, 58(4), 66–73.CrossRef
8.
Ramos, S. H., Villalba, M. T., & Lacuesta, R. (2018). MQTT security: A novel fuzzing approach. Wireless Communications and Mobile Computing, 2018.
9.
Houimli, M., Kahloul, L., Benaoun, S. (2017). Formal specification, verification and evaluation of the MQTT protocol in the internet of things. In: 2017 International conference on mathematics and information technology (ICMIT) (pp. 214–221).
10.
Mladenov, K., Mavrakis, C., van Winsen, S., & Cyber, K. P. M. G. (2017). Formal verification of the implementation of the MQTT protocol in IoT devices. Amsterdam: University of Amsterdam.
11.
Aziz, B. (2016). On the security of the MQTT protocol. p. 22.
12.
Diwan, M., & D’Souza, M. (2017). A framework for modeling and verifying IoT communication protocols. In: Dependable software engineering. Theories, tools, and applications: third international symposium, SETTA 2017, Proceedings (pp. 266–280). Changsha, China, October 23–25, 2017
13.
Tanabe, K., Tanabe, Y., & Hagiya, M. (2020). Model-based testing for MQTT applications. In M. Virvou, H. Nakagawa, & C. L. Jain (Eds.), Knowledge-based software engineering: 2020 (pp. 47–59). Cham: Springer.CrossRef
14.
15.
Araujo Rodriguez, L. G., & Macêdo Batista, D.: Program-aware fuzzing for MQTT applications. In: Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis. ISSTA 2020 (pp. 582–586). New York, NY, USA: Association for Computing Machinery (2020). https://​doi.​org/​10.​1145/​3395363.​3402645.
16.
Zahoor, E., Ikram, A., Akhtar, S., & Perrin, O. (2018). Authorization policies specification and consistency management within multi-cloud environments. Lecture Notes in Computer Science. In: N. Gruschka (ed.), Secure IT systems: 23rd Nordic conference, NordSec 2018, Proceedings (Vol. 11252, pp. 272–288). Oslo, Norway: Springer, November 28–30, 2018.
17.
Zahoor, E., Bibi, U., & Perrin, O. (2019). Shadowed authorization policies: A disaster waiting to happen? Lecture Notes in Computer Science. In R. Cheng, N. Mamoulis, Y. Sun, & X. Huang (Eds.), Web information systems engineering: WISE 2019—20th International Conference, Hong Kong, China, November 26–30, 2019, Proceedings (Vol. 11881, pp. 341–355). Hong Kong, China: Springer.
18.
Akhtar, S., Merz, S., & Quinson, M. (2010). A high-level language for modeling algorithms and their properties. In: 13th Brazilian symposium on formal methods (SBMF 2010). Natal: Springer.
19.
Yu, Y., Manolios, P., & Lamport, L. (1999). Model checking TLA+ specifications. In: Correct hardware design and verification methods (CHARME’99). Bad Herrenalb: Springer.
20.
Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press.MATH
21.
Akhtar, S., Zahoor, E., Perrin, O. (2017). Formal verification of authorization policies for enterprise social networks using PlusCal-2. In: CollaborateCom 2017: 13th EAI international conference on collaborative computing: networking, applications and worksharing, Edinburg, United Kingdom (pp. 1–10). https://​hal.​inria.​fr/​hal-01657116.
22.
Lamport, L. (2002). Specifying systems, the TLA+ language and tools for hardware and software engineers. Addison-Wesley.
23.
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., & Deardeuff, M. (2013). Use of formal methods at Amazon Web services.
24.
Akhtar, S. (2012). Formal verification of distributed algorithms using Pluscal-2. (vérification formelle d’algorithmes distribués en Pluscal-2). Ph.D. Thesis, University of Lorraine, Nancy, France.
25.
Holzmann, G., Peled, D.: An improvement in formal verification. In: IFIP WG 6.1 conference on formal description techniques (pp. 197–214). Bern: Chapman & Hall (1994)
Metadaten
Titel
Formal Specification and Verification of MQTT Protocol in PlusCal-2
verfasst von
Sabina Akhtar
Ehtesham Zahoor
Publikationsdatum
26.02.2021
Verlag
Springer US
Erschienen in
Wireless Personal Communications / Ausgabe 2/2021
Print ISSN: 0929-6212
Elektronische ISSN: 1572-834X
DOI
https://doi.org/10.1007/s11277-021-08296-4

Weitere Artikel der Ausgabe 2/2021

Wireless Personal Communications 2/2021 Zur Ausgabe

OriginalPaper

HAS-MAC: A Hybrid Asynchronous and Synchronous Communication System for Energy-Harvesting Wireless Sensor Networks

OriginalPaper

Distributed Adaptive Cooperative Bandwidth Spectrum Sensing for Cognitive MIMO Radios

OriginalPaper

Developing a Web Platform for the Management of the Predictive Maintenance in Smart Factories

OriginalPaper

Joint Statistical and Machine Learning Approach for Practical Data-Driven Assessment of User Throughput Quality in Microcellular Radio Networks

OriginalPaper

New Location Algorithm with Primary User Based on Scatter Information in Cognitive Radio

OriginalPaper

Lung Nodule Classification on Computed Tomography Images Using Fractalnet

Neuer Inhalt

    Bildnachweise