Skip to main content
SpringerLink
Log in
Book cover

International Conference on Model and Data Engineering

MEDI 2018: Model and Data Engineering pp 401–417Cite as

Ensuring the Functional Correctness of IoT through Formal Modeling and Verification

  • Conference paper
  • First Online:

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

Abstract

Recent research initiatives dedicated to formal modeling, functional correctness and security analysis of IoT systems, are generally limited to, model abstract behavioral patterns and look forward possible attacks beneath gauging and providing feasible attacks. This research considers the complementary problem by looking for more accurate attacks in IoT  by capturing richer behaviors -technical, physical, and social- including their quantitative features. We propose IoT-SEC  framework that establishes an adequate semantics to the IoT’s components and their interactions including social actors that behave differently than automated processes. For security analysis, we develop a general approach based on a library of attack trees from where we generate automatically the monitor, the security policies and requirements to harden the IoT model and to check how well the model is secure. We use PRISM model checker to analyze the functionality and to check security of the IoT model. Precisely this contribution ensures the functionality of IoT  systems by analyzing their functional correctness.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

  1. Abie, H.: Adaptive Security for the Internet of Things: Research, Standards, and Practices. 1st edn. Syngress Publishing (2017)

    Google Scholar 

  2. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, New York (2008)

    MATH  Google Scholar 

  3. Fink, G.A., Zarzhitsky, D.V., Carroll, T.E., Farquhar, E.D.: Security and privacy grand challenges for the Internet of Things. In: 2015 International Conference on Collaboration Technologies and Systems (CTS), pp. 27–34, June 2015

    Google Scholar 

  4. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International Incorporated, Upper Saddle River (1985)

    MATH  Google Scholar 

  5. Hu, P., Ning, H., Qiu, T., Song, H., Wang, Y., Yao, X.: Security and privacy preservation scheme of face identification and resolution framework using fog computing in Internet of Things. IEEE Int. Things J. 4(5), 1143–1155 (2017)

    Article  Google Scholar 

  6. Islam, S.M.R., Kwak, D., Kabir, M.H., Hossain, M., Kwak, K.S.: The internet of things for health care: a comprehensive survey. IEEE Access 3, 678–708 (2015)

    Article  Google Scholar 

  7. Kammüller, F., Augusto, J.C., Jones, S.: Security and privacy requirements engineering for human centric IoT systems using eFRIEND and isabelle. In: 2017 IEEE 15th International Conference on Software Engineering Research, Management and Applications (SERA), pp. 401–406, June 2017

    Google Scholar 

  8. Kammüller, F.: Formal modeling and analysis with humans in infrastructures for IoT health care systems. In: Tryfonas, T. (ed.) HAS 2017. LNCS, vol. 10292, pp. 339–352. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-58460-7_24

    Chapter  Google Scholar 

  9. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  10. Lenzini, G., Mauw, S., Ouchani, S.: Security analysis of socio-technical physical systems. Comput. Electr. Eng. 47, 258–274 (2015)

    Article  Google Scholar 

  11. Mohsin, M., Anwar, Z., Husari, G., Al-Shaer, E., Rahman, M.A.: IoTSAT: a formal framework for security analysis of the Internet of Things (IoT). In: 2016 IEEE Conference on Communications and Network Security (CNS), pp. 180–188, October 2016

    Google Scholar 

  12. Ouchani, S., Mohamed, O.A., Debbabi, M.: A security risk assessment framework for SysML activity diagrams. In: 2013 IEEE 7th International Conference on Software Security and Reliability (2013)

    Google Scholar 

  13. Ouchani, S., Ait Mohamed, O., Debbabi, M.: Efficient probabilistic abstraction for SysML activity diagrams. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 263–277. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_18

    Chapter  Google Scholar 

  14. Ouchani, S., Mohamed, O.A., Debbabi, M., Pourzandi, M.: Verification of the correctness in composed UML behavioural diagrams. In: Lee, R., Ormandjieva, O., Abran, A., Constantinides, C. (eds.) Software Engineering Research, Management and Applications 2010. Studies in Computational Intelligence, vol. 296, pp. 163–177. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13273-5_11

  15. Ould-Yahia, Y., Banerjee, S., Bouzefrane, S., Boucheneb, H.: Exploring formal strategy framework for the security in IoT towards e-health context using computational intelligence. In: Bhatt, C., Dey, N., Ashour, A.S. (eds.) Internet of Things and Big Data Technologies for Next Generation Healthcare. SBD, vol. 23, pp. 63–90. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-49736-5_4

    Chapter  Google Scholar 

  16. Torjusen, A.B., Abie, H., Paintsil, E., Trcek, D., Skomedal, Å.: Towards run-time verification of adaptive security for IoT in ehealth. In: Proceedings of the 2014 European Conference on Software Architecture Workshops, ECSAW 2014, pp. 4:1–4:8. ACM (2014)

    Google Scholar 

  17. Xu, T., Wendt, J.B., Potkonjak, M.: Security of IoT systems: design challenges and opportunities. In: Proceedings of the 2014 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2014, pp. 417–423. IEEE Press (2014)

    Google Scholar 

  18. Zhang, Z.K., Cho, M.C.Y., Wang, C.W., Hsu, C.W., Chen, C.K., Shieh, S.: IoT security: ongoing challenges and research opportunities. In: 2014 IEEE 7th International Conference on Service-Oriented Computing and Applications, pp. 230–234, November 2014

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LINEACT, Laboratoire d’Innovation Numérique, École d’Ingénieur en Informatique, CESI eXia, Aix-en-Provence, France

    Samir Ouchani

Authors
  1. Samir Ouchani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Samir Ouchani .

Editor information

Editors and Affiliations

  1. Cadi Ayyad University, Marrakesh, Morocco

    El Hassan Abdelwahed

  2. LIAS/ISAE-ENSMA, Futuroscope Chasseneuil Cedex, France

    Ladjel Bellatreche

  3. University of Bologna, Cesena, Italy

    Mattéo Golfarelli

  4. University of Lorraine, Vandœuvre-lès-Nancy, France

    Dominique Méry

  5. University of Houston, Houston, TX, USA

    Carlos Ordonez

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ouchani, S. (2018). Ensuring the Functional Correctness of IoT through Formal Modeling and Verification. In: Abdelwahed, E., Bellatreche, L., Golfarelli, M., Méry, D., Ordonez, C. (eds) Model and Data Engineering. MEDI 2018. Lecture Notes in Computer Science(), vol 11163. Springer, Cham. https://doi.org/10.1007/978-3-030-00856-7_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00856-7_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00855-0

  • Online ISBN: 978-3-030-00856-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation