Skip to main content
SpringerLink
Log in

A Framework for Modeling and Verifying IoT Communication Protocols

  • Conference paper
  • First Online:
Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10606))

Abstract

Communication protocols are integral part of the ubiquitous IoT. There are numerous light-weight protocols with small footprint available in the Industry. However, they have no formal semantics and are not formally verified. Since these protocols have many common features, we propose a unified approach to verify these protocols through a framework in Event-B. We begin with an abstract model of an IoT communication protocol which encompasses common features of various protocols. The abstract model is then refined into concrete models for individual IoT protocols using refinement and decomposition techniques of Event-B. Using the above framework, we present models of MQTT, MQTT-SN and CoAP protocols, and verify communication properties like connection-establishment, persistent-sessions, caching, proxying, message ordering, QoS, etc. Our protocol models can be integrated-with or extended-to other formal models of IoT systems using machine-decomposition within Event-B, thus paving way for formal modeling and verification of IoT systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Event-B. http://www.Event-B.org/

  2. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  3. 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–235. Springer, Heidelberg (2006). doi:10.1007/11813040_16

    Chapter  Google Scholar 

  4. Rodin Tool. http://wiki.Event-B.org/index.php/Rodin_Platform

  5. Rodin Hand Book. https://www3.hhu.de/stups/handbook/rodin/current/pdf/rodin-doc.pdf

  6. ProB tool. https://www3.hhu.de/stups/prob/index.php/Main_Page

  7. Gartner newsroom. http://www.gartner.com/newsroom/id/3165317

  8. 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–7 (2015)

    Google Scholar 

  9. MQTT Ver. 3.1.1. http://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html

  10. MQTT-SN Ver. 1.2. http://mqtt.org/new/wp-content/uploads/2009/06/MQTT-SN_spec_v1.2.pdf

  11. The Constrained Application Protocol (CoAP) RFC7252. https://tools.ietf.org/html/rfc7252

  12. Extensible Messaging and Presence Protocol (XMPP) Core RFC6120. http://xmpp.org/rfcs/rfc6120.html

  13. Advanced Message Queuing Protocol ver. 1.0. http://docs.oasis-open.org/amqp/core/v1.0/amqp-core-complete-v1.0.pdf

  14. Pascal, C., Renato, S.: Event-B model decomposition, DEPLOY Plenary Technical Workshop (2009)

    Google Scholar 

  15. 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–93. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33826-7_6

    Chapter  Google Scholar 

  16. Aziz, B.: A formal model and analysis of the MQ telemetry transport protocol. In: Ninth International Conference, Availability, Reliability and Security (ARES), pp. 59–68. Fribourg (2014)

    Google Scholar 

  17. Gawanmeh, A.: Embedding and verification of ZigBee protocol stack in Event-B. In: Procedia Computer Science, vol. 5, pp. 736–741. ISSN 1877–0509 (2011)

    Google Scholar 

  18. 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–684. IEEE Press (2013)

    Google Scholar 

  19. 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–717. IEEE (2013)

    Google Scholar 

  20. 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–6. IEEE Press (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. International Institute of Information Technology, Bangalore, India

    Maithily Diwan & Meenakshi D’Souza

Authors
  1. Maithily Diwan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Meenakshi D’Souza
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Meenakshi D’Souza .

Editor information

Editors and Affiliations

  1. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen

  2. University of Pennsylvania, Philadelphia, Pennsylvania, USA

    Oleg Sokolsky

  3. National University of Defense Technology, Changsha, China

    Ji Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Diwan, M., D’Souza, M. (2017). A Framework for Modeling and Verifying IoT Communication Protocols. In: Larsen, K., Sokolsky, O., Wang, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2017. Lecture Notes in Computer Science(), vol 10606. Springer, Cham. https://doi.org/10.1007/978-3-319-69483-2_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-69483-2_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-69482-5

  • Online ISBN: 978-3-319-69483-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation