Abstract
In recent years, Internet of Things (IoT) has been one of the most popular technologies that facilitate new interactions among things and humans to enhance the quality of life. With the rapid development of the IoT, Industrial and enterprise IoT are emerging as an attractive solution for processing the IoT applications. On the other hand, due to the guarantee of safety-critical conditions without system failures in smart devices, formal verification approaches are essential to manage and evaluate critical failures and reachable status in these problems. In this paper, a review of the formal verification approaches in the IoT applications is presented to recognize the state-of-the-art mechanisms on this important topic. The formal verification approaches of the IoT environments are compared with each other according to the advantages and limitations.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Ahmad S, Malik S, Ullah I, Park DH, Kim K, & Kim D (2019). Towards the Design of a Formal Verification and Evaluation Tool of Real-Time Tasks Scheduling of IoT Applications. Sustainability 11(1): 204.
Aktas MS, & Astekin M (2019) Provenance aware run-time verification of things for self-healing Internet of Things applications. Concurrency and Computation: Practice and Experience, e4263-n/a. DOI: https://doi.org/10.1002/cpe.4263.
Ali MS, Jewel MKH, Li Y, & Lin F (2019) Frequency-domain channel equalisation for LTE-based uplink narrowband Internet of Things systems. IET Communications 13(3): 281–288. https://digital-library.theiet.org/content/journals/10.1049/iet-com.2018.5119
Asghari P, Rahmani AM, & Javadi HHS (2018) Service composition approaches in IoT: A systematic review. Journal of Network and Computer Applications 120: 61–77. doi: https://doi.org/10.1016/j.jnca.2018.07.013.
Asghari P, Rahmani AM, & Javadi HHS (2019). Internet of Things applications: A systematic review. Computer Networks 148: 241–261.
Aziz B (2016) A formal model and analysis of an IoT protocol. Ad Hoc Networks 36: 49–57.
Bae WS (2017) Verifying a secure authentication protocol for IoT medical devices. Cluster Computing. DOI: https://doi.org/10.1007/s10586-017-1107-x.
Deng Y, Chen Z, Zhang D, & Zhao M (2018) Workload scheduling toward worst-case delay and optimal utility for single-hop Fog-IoT architecture. IET Communications 12(17): 2164–2173.
Desnitsky V & Kotenko I (2016) Automated design, verification and testing of secure systems with embedded devices based on elicitation of expert knowledge. Journal of Ambient Intelligence and Humanized Computing 7(5): 705–719.
Dhillon PK & Kalra S (2017a) A lightweight biometrics based remote user authentication scheme for IoT services. Journal of Information Security and Applications 34: 255–270.
Dhillon PK & Kalra S (2017b) Secure multi-factor remote user authentication scheme for Internet of Things environments. International Journal of Communication Systems 30(16): e3323-n/a.
Diwan M & D’Souza M (2017) A Framework for Modeling and Verifying IoT Communication Protocols. In K. G. Larsen, O. Sokolsky & J. Wang (Eds.), Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, Proceedings (pp. 266–280). Cham: Springer International Publishing.
Drozdov D, Patil S, Dubinin V, & Vyatkin V (2017) Towards formal verification for cyber-physically agnostic software: A case study. Paper presented at the IECON 2017 — 43rd Annual Conference of the IEEE Industrial Electronics Society.
Elleuch M, Hasan O, Tahar S, & Abid M. (2017) Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications. In C. Artho & P. C. Ölveczky (Eds.), Formal Techniques for Safety-Critical Systems: 5th International Workshop, FTSCS 2016, Tokyo, Japan, November 14, 2016, Revised Selected Papers (pp. 93–108). Cham: Springer International Publishing.
Ghobaei-Arani M, Rahmanian AA, Souri A, & Rahmani AM (2018) A moth-flame optimization algorithm for web service composition in cloud computing: Simulation and verification. Software: Practice and Experience, 48(10): 1865–1892.
Hameed K, Khan A, Ahmed M, Goutham Reddy A, & Rathore MM (2017) Towards a formally verified zero watermarking scheme for data integrity in the Internet of Things based-wireless sensor networks. Future Generation Computer Systems. doi: https://doi.org/10.1016/j.future.2017.12.009.
Han KH, & Bae WS (2016) Proposing and verifying a security-enhanced protocol for IoT-based communication for medical devices. Cluster Computing 19(4): 2335–2341.
Kammüller F (2017) Formal Modeling and Analysis with Humans in Infrastructures for IoT Health Care Systems. In T. Tryfonas (Ed.), Human Aspects of Information Security, Privacy and Trust: 5th International Conference, HAS 2017, Held as Part of HCI International 2017, Vancouver, BC, Canada, July 9–14, 2017, Proceedings (pp. 339–352). Cham: Springer International Publishing.
Kammüller F (2018) Human Centric Security and Privacy for the IoT Using Formal Techniques. In D. Nicholson (Ed.), Advances in Human Factors in Cybersecurity: Proceedings of the AHFE 2017 International Conference on Human Factors in Cybersecurity, July 17–21, 2017, The Westin Bonaventure Hotel, Los Angeles, California, USA (pp. 106–116). Cham: Springer International Publishing.
Kim H, Kang E, Lee EA, & Broman D (2017) A Toolkit for Construction of Authorization Service Infrastructure for the Internet of Things. Paper presented at the 2017 IEEE/ACM Second International Conference on Internet-of-Things Design and Implementation (IoTDI).
La HJ (2016) A conceptual framework for trajectory-based medical analytics with IoT contexts. Journal of Computer and System Sciences 82(4): 610–626.
Lanotte R & Merro M (2018) A semantic theory of the Internet of Things. Information and Computation 259: 72–101.
Mangano F, Duquennoy S, & Kosmatov N. (2017) Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. In F. Cuppens, N. Cuppens, J.-L. Lanet & A. Legay (Eds.), Risks and Security of Internet and Systems: 11th International Conference, CRiSIS 2016, Roscoff, France, September 5–7, 2016, Revised Selected Papers (pp. 114–120). Cham: Springer International Publishing.
Mohsin M, Sardar MU, Hasan O, & Anwar Z (2017) IoTRiskAnalyzer: A Probabilistic Model Checking Based Framework for Formal Risk Analytics of the Internet of Things. IEEE Access 5: 5494–5505.
Nishiwaki Y (2016) F-Calculus: A Universal Programming Language of Self-Stabilizing Computational Fields. Paper presented at the 2016 IEEE 1st International Workshops on Foundations and Applications of Self* Systems (FAS*W).
Ouaddah A, Abou Elkalam A, & Ait Ouahman A (2016) FairAccess: a new Blockchain-based access control framework for the Internet of Things. Security and Communication Networks 9(18): 5943–5964.
Perković T, Čagalj M, & Kovačević T (2019) LISA: Visible light based initialization and SMS based authentication of constrained IoT devices. Future Generation Computer Systems.
Saxena D & Raychoudhury V (2017) Design and Verification of an NDN-Based Safety-Critical Application: A Case Study With Smart Healthcare. IEEE Transactions on Systems, Man, and Cybernetics: Systems 99: 1–15.
Souri A, Asghari P, & Rezaei R (2017) Software as a service based CRM providers in the cloud computing: Challenges and technical issues. Journal of Service Science Research 9(2): 219–237.
Souri A, Norouzi M, Safarkhanlou A, & Sardroud SHEH (2016) A dynamic data replication with consistency approach in data grids: modeling and verification. Baltic Journal of Modern Computing 4(3): 546.
Souri A, Nourozi M, Rahmani AM, & Jafari Navimipour N (2018a) A model checking approach for user relationship management in the social network. Kybernetes 48(3): 407–423.
Souri A, Rahmani, AM, & Jafari Navimipour N (2018b), Formal verification approaches in the web service composition: A comprehensive analysis of the current challenges for future research. International Journal of Communication Systems 31(17): e3808.
Souri A, Rahmani AM, Navimipour NJ, & Rezaei, R. (2019) Formal modeling and verification of a service composition approach in the social customer relationship management system. Information Technology & People, (Earlycite) https://doi.org/10.1108/ITP-02-2018-0109.
Souri A, Rahmani AM, Navimipour NJ, & Rezaei R (2019) A symbolic model checking approach in formal verification of distributed systems. Human-centric Computing and Information Sciences 9(1): 4. DOI: https://doi.org/10.1186/s13673-019-0165-x.
Tata S, Klai K, & Jain R (2017) Formal Model and Method to Decompose Process-Aware IoT Applications. In H. Panetto, C. Debruyne, W. Gaaloul, M. Papazoglou, A. Paschke, C. A. Ardagna & R. Meersman (Eds.), On the Move to Meaningful Internet Systems. OTM 2017 Conferences: Confederated International Conferences: CoopIS, C&TC, and ODBASE 2017, Rhodes, Greece, October 23–27, 2017, Proceedings, Part I (pp. 663–680). Cham: Springer International Publishing.
Venckauskas A, Stuikys V, Damasevicius R, & Jusas N (2016) Modelling of Internet of Things units for estimating security-energy-performance relationships for quality of service and environment awareness. Security and Communication Networks 9(16): 3324–3339.
Xu S, Miao W, Kunz T, Wei T, & Chen M (2016) Quantitative Analysis of Variation-Aware Internet of Things Designs Using Statistical Model Checking. Paper presented at the +2016 IEEE International Conference on Software Quality, Reliability and Security (QRS).
Zahra S, Alam M, Javaid Q, Wahid A, Javaid N, Malik SUR, & Khan MK (2017) Fog Computing Over IoT: A Secure Deployment and Formal Verification. IEEE Access 5: 27132–27144.
Zhang Y & Chen JL (2015) Constructing scalable Internet of Things services based on their event-driven models. Concurrency and Computation: Practice and Experience 27(17): 4819–4851.
Author information
Authors and Affiliations
Corresponding author
Additional information
Alireza Souri received his B.S. degree in Software Engineering from University College of Nabi Akram, Iran, in 2011 and his M.Sc. and PhD degrees in Software Engineering from Science and Research Branch, Islamic Azad University, Iran in 2013 and 2018. He is a researcher and lecturer at Islamic Azad University. Up to now, he has authored/co-authored 40 academic articles. He served on the program committees and the technical reviewer of several ISI-index journals and international conferences. He currently is an Associate Editor member of Human-Centric Computing and Information Sciences (Springer), Cluster Computing (Springer) and IET Communications (IEEE) journals. His research interests include Formal Specification & Verification, Model checking, Grid & Cloud computing, IoT and Social networks. Now, He is a member of The Society of Digital Information and Wireless Communications.
Monire Norouzi received her B.Sc. in Computer Engineering at University College of Nabi Akram, Iran in 2011. She received M.Sc. in Software Engineering from Shabestar Branch, Islamic Azad University in Iran. Her main research interests are Software Analysis, Wireless Network and Sensor Network, verification and validation of Software Systems.
Rights and permissions
About this article
Cite this article
Souri, A., Norouzi, M. A State-of-the-Art Survey on Formal Verification of the Internet of Things Applications. J Serv Sci Res 11, 47–67 (2019). https://doi.org/10.1007/s12927-019-0003-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s12927-019-0003-8