A Survey on Formal Verification and Validation Techniques for Internet of Things
Source abstract
Abstract
The Internet of Things (IoT) has brought about a new era of connected devices and systems, with applications ranging from healthcare to transportation. However, the reliability and security of these systems are critical concerns that must be addressed to ensure their safe and effective operation. This paper presents a survey of formal verification and validation (FV&V) techniques for IoT systems, with a focus on the challenges and open issues in this field. We provide an overview of formal methods and testing techniques for the IoT and discuss the state explosion problem and techniques to address it. We also examined the use of AI in software testing and describe examples of tools that use AI in this context. Finally, we discuss the challenges and open issues in FV&V for the IoT and present possible future directions for research. This survey paper aimed to provide a comprehensive understanding of the current state of FV&V techniques for IoT systems and to highlight areas for further research and development.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Software Testing and Debugging Techniques · Advanced Malware Detection Techniques · Software Reliability and Analysis Research
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
Faculty of Computer Science and Information Technology, Al-Baha University, Al-Baha 65528, Saudi Arabia
ReDCAD Laboratory, University of Sfax, Sfax 3038, Tunisia
References (85)
Show source-provided references
1. A review and state of art of Internet of Things (IoT)10.1007/s11831-021-09622-6 ↗
2. Toward Secured IoT-Based Smart Systems Using Machine Learning10.1109/ACCESS.2023.3250235 ↗
3. Fusion of multivariate EEG signals for schizophrenia detection using CNN and machine learning techniques10.1016/j.inffus.2022.12.019 ↗
4. Efficient Approach for Anomaly Detection in Internet of Things Traffic Using Deep Learning10.1155/2022/8266347 ↗
5. Alamer, M., and Almaiah, M.A. (2021, January 14–15). Cybersecurity in Smart City: A systematic mapping study. Proceedings of the 2021 International Conference on Information Technology (ICIT), Amman, Jordan.10.1109/ICIT52682.2021.9491123 ↗
6. Allouch, A., Cheikhrouhou, O., Koubâa, A., Toumi, K., Khalgui, M., and Nguyen Gia, T. (2021). Utm-chain: Blockchain-based secure unmanned traffic management for Internet of drones. Sensors, 21.10.3390/s21093049 ↗
7. Abdalzaher, M.S., Salim, M.M., Elsayed, H.A., and Fouda, M.M. (2022, January 24–26). Machine learning benchmarking for secured IoT smart systems. Proceedings of the 2022 IEEE International Conference on Internet of Things and Intelligence Systems (IoTaIS), Bali, Indonesia.10.1109/IoTaIS56727.2022.9975952 ↗
8. An Efficient Approach for the Detection and Prevention of Gray-Hole Attacks in VANETs10.1109/ACCESS.2023.3274650 ↗
9. Employing remote sensing, data communication networks, ai, and optimization methodologies in seismology10.1109/JSTARS.2022.3216998 ↗
10. Lee, I. (2020). Internet of Things (IoT) cybersecurity: Literature review and IoT cyber risk management. Future Internet, 12.10.3390/fi12090157 ↗
11. Koubaa, A., Allouche, A., Khalgui, M., and Cheikhrouhou, O. (2022). Blockchain-Based Solution for Internet of Drones Security and Privacy. (11,488,488), U.S. Patent.
12. Future smart cities: Requirements, emerging technologies, applications, challenges, and future aspects10.1016/j.cities.2022.103794 ↗
13. Antonakakis, M., April, T., Bailey, M., Bernhard, M., Bursztein, E., Cochran, J., Durumeric, Z., Halderman, J.A., Invernizzi, L., and Kallitsis, M. (2017, January 16–18). Understanding the Mirai Botnet. Proceedings of the 26th USENIX Security Symposium (USENIX Security 17), Vancouver, BC, Canada.
14. Bakić, B., Milić, M., Antović, I., Savić, D., and Stojanović, T. (2021, January 16–20). 10 years since Stuxnet: What have we learned from this mysterious computer software worm?. Proceedings of the 2021 25th International Conference on Information Technology (IT), Zabljak, Montenegro.10.1109/IT51528.2021.9390103 ↗
15. Survey on learning-based formal methods: Taxonomy, applications and possible future directions10.1109/ACCESS.2020.3000907 ↗
16. Formal methods in dependable systems engineering: A survey of professionals from Europe and North America10.1007/s10664-020-09836-5 ↗
17. New opportunities for integrated formal methods10.1145/3357231 ↗
18. Hofer-Schmitz, K., and Stojanović, B. (2019, January 28–29). Towards formal methods of IoT application layer protocols. Proceedings of the 2019 12th CMI Conference on Cybersecurity and Privacy (CMI), Copenhagen, Denmark.10.1109/CMI48017.2019.8962139 ↗
19. A state-of-the-art survey on formal verification of the Internet of things applications10.1007/s12927-019-0003-8 ↗
20. Security testbed for Internet-of-Things devices10.1109/TR.2018.2864536 ↗
21. Jeannotte, B., and Tekeoglu, A. (2019, January 8–10). Artorias: IoT security testing framework. Proceedings of the 2019 26th International Conference on Telecommunications (ICT), Hanoi, Vietnam.10.1109/ICT.2019.8798846 ↗
22. Risk-based automated assessment and testing for the cybersecurity certification and labelling of IoT devices10.1016/j.csi.2018.08.003 ↗
23. Model-based testing in practice: An experience report from the web applications domain10.1016/j.jss.2021.111032 ↗
24. Model-based testing using UML activity diagrams: A systematic mapping study10.1016/j.cosrev.2019.07.001 ↗
25. A formal testing model for operating room control system using Internet of things
26. The relevance of classic fuzz testing: Have we solved this one?10.1109/TSE.2020.3047766 ↗
27. Fu, Y., Ren, M., Ma, F., Shi, H., Yang, X., Jiang, Y., Li, H., and Shi, X. (2019, January 26–30). Evmfuzzer: Detect evm vulnerabilities via fuzz testing. Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Tallinn, Estonia.10.1145/3338906.3341175 ↗
28. Mihalič, F., Truntič, M., and Hren, A. (2022). Hardware-in-the-loop simulations: A historical overview of engineering challenges. Electronics, 11.10.3390/electronics11152462 ↗
29. Kiesbye, J., Messmann, D., Preisinger, M., Reina, G., Nagy, D., Schummer, F., Mostad, M., Kale, T., and Langer, M. (2019). Hardware-in-the-loop and software-in-the-loop testing of the move-ii cubesat. Aerospace, 6.10.3390/aerospace6120130 ↗
30. Design and hardware-in-the-loop test of a coupled drive system for electric tractor10.1016/j.biosystemseng.2022.02.014 ↗
31. Towards formal verification of IoT protocols: A Review10.1016/j.comnet.2020.107233 ↗
32. Al Farooq, A., Al-Shaer, E., Moyer, T., and Kant, K. (2019, January 8–12). Iotc 2: A formal method approach for detecting conflicts in large scale iot systems. Proceedings of the 2019 IFIP/IEEE symposium on integrated network and service management (IM), Arlington, VA, USA.
33. Ahmed, A.I.A., Hamid, S.H.A., Gani, A., Abdelaziz, A., and Abaker, M. (2023). Formal Analysis of Trust and Reputation for Service Composition in IoT. Sensors, 23.10.3390/s23063192 ↗
34. Souad, M., Faiza, B., and Nabil, H. (2020, January 28–30). Formal modeling iot systems on the basis of biagents* and maude. Proceedings of the 2020 International Conference on Advanced Aspects of Software Engineering (ICAASE), Constantine, Algeria.10.1109/ICAASE51408.2020.9380126 ↗
35. A formal model and analysis of an IoT protocol10.1016/j.adhoc.2015.05.013 ↗
36. Formal verification of IoT applications using rewriting logic: An MDE-based approach10.1016/j.scico.2022.102859 ↗
37. Hagar, J., and Wendland, M.F. (2023, January 16–20). Defining Software Test Architectures with the UML Testing Profile. Proceedings of the 2023 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), Dublin, Ireland.10.1109/ICSTW58534.2023.00056 ↗
38. Toman, Z.H., Hamel, L., Toman, S.H., Graiet, M., and Valadares, D.C.G. (2023). Formal verification for security and attacks in IoT physical layer. J. Reliab. Intell. Environ., 1–19.10.1007/s40860-023-00202-y ↗
39. Formal Verification of an Efficient Architecture to Enhance the Security in IoT
40. Keerthi, K., Roy, I., Hazra, A., and Rebeiro, C. (2019). Formal verification for security in IoT devices. Secur. Fault Toler. Internet Things, 179–200.10.1007/978-3-030-02807-7_9 ↗
41. Shieh, M.Z., Lin, Y.B., and Hsu, Y.J. (2021). VerificationTalk: A verification and security mechanism for IoT applications. Sensors, 21.10.3390/s21227449 ↗
42. Non-zero-sum game-based trust model to enhance wireless sensor networks security for IoT applications10.1049/iet-wss.2018.5114 ↗
43. Cheikhrouhou, O., and Koubâa, A. (2019, January 24–28). Blockloc: Secure localization in the Internet of things using blockchain. Proceedings of the 2019 15th International Wireless Communications & Mobile Computing Conference (IWCMC), Tangier, Morocco.10.1109/IWCMC.2019.8766440 ↗
44. Feature engineering and deep learning-based intrusion detection framework for securing edge IoT10.1007/s11227-021-04250-0 ↗
45. Ahmad, W., Rasool, A., Javed, A.R., Baker, T., and Jalil, Z. (2021). Cyber security in IoT-based cloud computing: A comprehensive survey. Electronics, 11.10.3390/electronics11010016 ↗
46. Mihoub, A., and Lefebvre, G. (2017, January 13–16). Social intelligence modeling using wearable devices. Proceedings of the 22nd International Conference on Intelligent User Interfaces, Limassol, Cyprus.10.1145/3025171.3025195 ↗
47. Kelati, A., Dhaou, I.B., and Tenhunen, H. (2018, January 15–18). Biosignal monitoring platform using Wearable IoT. Proceedings of the 22st Conference of Open Innovations Association FRUCT, Jyvaskyla, Finland.
48. A deep learning model for earthquake parameters observation in IoT system-based earthquake early warning10.1109/JIOT.2021.3114420 ↗
49. Hybrid EEG-fNIRS brain-computer interface based on the non-linear features extraction and stacking ensemble learning10.1016/j.bbe.2023.05.001 ↗
50. Krichen, M., Adoni, W.Y.H., Mihoub, A., Alzahrani, M.Y., and Nahhal, T. (2022, January 9–11). Security challenges for drone communications: Possible threats, attacks and countermeasures. Proceedings of the 2022 2nd International Conference of Smart Systems and Emerging Technologies (SMARTTECH), Riyadh, Saudi Arabia.10.1109/SMARTTECH54121.2022.00048 ↗
51. Real time performance analysis of secure IoT protocols for microgrid communication10.1016/j.future.2020.09.031 ↗
52. Gupta, M., Kumar, R., Shekhar, S., Sharma, B., Patel, R.B., Jain, S., Dhaou, I.B., and Iwendi, C. (2022). Game theory-based authentication framework to secure Internet of vehicles with blockchain. Sensors, 22.10.3390/s22145119 ↗
53. Cousot, P. (2001). Informatics: 10 Years Back. 10 Years Ahead, Springer.
54. Gosain, A., and Sharma, G. (2015). Intelligent Computing and Applications, Springer.
55. Saadatmand, M., Enoiu, E.P., Schlingloff, H., Felderer, M., and Afzal, W. (September, January 31). Smartdelta: Automated quality assurance and optimization in incremental industrial software systems development. Proceedings of the 2022 25th Euromicro Conference on Digital System Design (DSD), Maspalomas, Spain.10.1109/DSD57027.2022.00106 ↗
56. Abbas, M., Hamayouni, A., Moghadam, M.H., Saadatmand, M., and Strandberg, P.E. (2023, January 24–26). Making Sense of Failure Logs in an Industrial DevOps Environment. Proceedings of the International Conference on Information Technology-New Generations, Las Vegas, NV, USA.10.1007/978-3-031-28332-1_25 ↗
57. Müller-Olm, M., Schmidt, D., and Steffen, B. (1999, January 22–24). Model-checking. Proceedings of the International Static Analysis Symposium, Venice, Italy.10.1007/3-540-48294-6_22 ↗
58. Proof assistants: History, ideas and future10.1007/s12046-009-0001-5 ↗
59. Pnueli, A., Ruah, S., and Zuck, L. (2001, January 2–6). Automatic deductive verification with invisible invariants. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Genoa, Italy.10.1007/3-540-45319-9_7 ↗
60. Burch, J.R., Passerone, R., and Sangiovanni-Vincentelli, A.L. (2003). System Specification & Design Languages, Springer.
61. Bensalem, S., Krichen, M., Majdoub, L., Robbana, R., and Tripakis, S. (2007, January 12–14). A Simplified Approach for Testing Real-Time Systems Based on Action Refinement. Proceedings of the ISoLA 2007, Workshop on Leveraging Applications of Formal Methods, Verification and Validation, Poitiers, France.
62. Krichen, M. (2018). Contributions to Model-Based Testing of Dynamic and Distributed Real-Time Systems. [Ph.D. Thesis, École Nationale d’Ingénieurs de Sfax].
63. Krichen, M. (2010, January 14–17). A formal framework for conformance testing of distributed real-time systems. Proceedings of the International Conference on Principles of Distributed Systems, Tozeur, Tunisia.10.1007/978-3-642-17653-1_12 ↗
64. Davis, J.A., Clark, M., Cofer, D., Fifarek, A., Hinchman, J., Hoffman, J., Hulbert, B., Miller, S.P., and Wagner, L. (2013, January 23–24). Study on the barriers to the industrial adoption of formal methods. Proceedings of the International Workshop on Formal Methods for Industrial Critical Systems, Madrid, Spain.10.1007/978-3-642-41010-9_5 ↗
65. Barrett, C., and Tinelli, C. (2018). Handbook of Model Checking, Springer.
66. Formal methods for verification and validation of partial specifications: A case study10.1016/S0164-1212(97)00167-2 ↗
67. Khorikov, V. (2020). Unit Testing Principles, Practices, and Patterns, Simon and Schuster.
68. Shashank, S.P., Chakka, P., and Kumar, D.V. (2010, January 17–19). A systematic literature survey of integration testing in component-based software engineering. Proceedings of the 2010 International Conference on Computer and Communication Technology (ICCCT), Allahabad, India.10.1109/ICCCT.2010.5640467 ↗
69. Van Heugten Breurkes, J., Gilson, F., and Galster, M. (2022, January 13–15). Overlap between Automated Unit and Acceptance Testing—A Systematic Literature Review. Proceedings of the International Conference on Evaluation and Assessment in Software Engineering 2022, Gothenburg, Sweden.10.1145/3530019.3530028 ↗
70. Automated functional testing of mobile applications: A systematic mapping study10.1007/s11219-018-9418-6 ↗
71. Hertzum, M. (2020). Usability Testing: A Practitioner’s Guide to Evaluating the User Experience, Springer. Synthesis Lectures on Human-Centered Informatics.10.1007/978-3-031-02227-2 ↗
72. Maâlej, A.J., Lahami, M., Krichen, M., and Jmaïel, M. (2018, January 21–24). Distributed and Resource-Aware Load Testing of WS-BPEL Compositions. Proceedings of the 20th International Conference on Enterprise Information Systems (ICEIS 2018), Funchal, Portugal.
73. Performance testing as a service using cloud computing environment: A survey10.1002/smr.2492 ↗
74. A survey on runtime testing of dynamically adaptable and distributed systems10.1007/s11219-021-09558-x ↗
75. Holzinger, A., Saranti, A., Angerschmid, A., Retzlaff, C.O., Gronauer, A., Pejakovic, V., Medel-Jimenez, F., Krexner, T., Gollob, C., and Stampfer, K. (2022). Digital transformation in smart farm and forest operations needs human-centered AI: Challenges and future directions. Sensors, 22.10.3390/s22083043 ↗
76. Monitoring social distancing using artificial intelligence for fighting COVID-19 virus spread10.4018/IJOSSP.2021070104 ↗
77. Krichen, M., Mihoub, A., Alzahrani, M.Y., Adoni, W.Y.H., and Nahhal, T. (2022, January 9–11). Are Formal Methods Applicable To Machine Learning And Artificial Intelligence?. Proceedings of the 2022 2nd International Conference of Smart Systems and Emerging Technologies (SMARTTECH), Riyadh, Saudi Arabia.10.1109/SMARTTECH54121.2022.00025 ↗
78. A deep learning-based framework for human activity recognition in smart homes
79. A survey on software testing techniques using artificial intelligence
80. A survey on software testing with machine learning
81. Tuberculosis disease diagnosis based on an optimized machine learning model10.1155/2022/8950243 ↗
82. Agricultural decision system based on advanced machine learning models for yield prediction: Case of East African countries10.1016/j.atech.2022.100048 ↗
83. Crops yield prediction based on machine learning models: Case of West African countries10.1016/j.atech.2022.100049 ↗
84. Theft detection dataset for benchmarking and machine learning based classification in a smart grid environment
85. Teodoraș, D.A., Popovici, E.C., Suciu, G., and Sachian, M.A. (2022, January 25–28). Quantum technology’s role in cyber-security. Proceedings of the Advanced Topics in Optoelectronics, Microelectronics, and Nanotechnologies XI, Constanta, Romania.10.1117/12.2643300 ↗