Formal Verification Approach for IoT Conflict Resolution by Priority
DOI:
https://doi.org/10.29304/jqcsm.2026.18.12640Keywords:
Conflict detect, Conflict resolutionAbstract
Internet of Things (IoT)-based solutions, especially automation systems, are essential for controlling networked devices and creating adaptive and intelligent environments. End-user-developed IoT services/apps interact and share simultaneous access to devices depending on their preferences, thereby increasing safety, security, and correctness issues. System failures or reduced performance might result from the traditional reactive approach to dispute resolution, which identifies and fixes problems after they have already happened. To tackle important issues, IoT-based applications require special tools to check and analyse their design, helping to find problems and conflicts in the instructions and interactions of IoT applications. This paper employs the Event-B formal method to introduce a novel approach for detecting and resolution conflicts in IoT systems by using priority. To systematically identify and resolve any conflicts, formal models of the IoT system are developed and refined using abstraction and refinement techniques. The objective of this paper is to promote the use of formal Event-B modelling and verification during the initial stages of the development of an IoT system to expedite the detection and fixing of problems. The proposed model addresses several types of conflicts, such as resource, functional, priority, and policy conflicts. The Rodin platform automates verification, ensuring that all declared invariants and attributes are preserved during system operation. As an example of our method in action, we will take a look at an ECG IoT system. The model accurately detects possible conflicts in these situations. We verify our method using the Rodin model checking tool, proof obligations and the ProB animator.
Downloads
References
Ryan, P.J., Watson, R.B.: Research challenges for the internet of things: what role can or play? Systems 5(1), 24 (2017)
Va¨yrynen, R.: Regional conflict formations: an intractable problem of international relations. J. Peace Res. 21(4), 337–359
(1984)
Mohammed, I. A. (2022). A comprehensive mapping research on the management of conflicts in IoT-based systems actuation toward DevOps.
Pradeep, P., Kant, K.: Conflict detection and resolution in IoT systems: a survey. IoT 3(1), 191–218 (2022)
Huang, B., Chen, C., Lam, K. Y., & Huang, F. (2024, July). Proactive Detection of Physical Inter-rule Vulnerabilities in IoT Services Using a Deep Learning Approach. In 2024 IEEE International Conference on Web Services (ICWS) (pp. 164-171). IEEE.
Toman, S.H., Hamel, L., Toman, Z.H., Graiet, M., Ouchani, S.:Formal modelling and verification of scalable service composition in IoT environment. SOCA 17(3), 213–231 (2023)
Abrial, J.R.: On b and Event-B: principles, success and challenges.In: Abstract State Machines, Alloy, B, TLA, VDM, and Z: 6th International Conference, ABZ 2018, Southampton, UK, June 5–8, 2018, Proceedings 6, pp. 31–35. Springer (2018)
Wing,J. M.(1990).A specifier's introduction to formal methods.Computer,23(9),8-22.
Toman, S.H., Hamel, L., Graiet, M.: Refinement and verification for IoT service composition. In: 2023 IEEE Symposium on Computers and Communications (ISCC), pp. 483–486 (2023). https://doi.org/10.1109/ISCC58397.2023.10218287
Toman, Z.H., Hamel, L., Toman, S.H., Graiet, M., Valadares, D.C.G.: Formal verification for security and attacks in IoT physical layer. J. Reliab. Intell. Environ. 2021, 1–19 (2023)
Toman, S.H., Lahouij, A., Hamel, L., Toman, Z.H., Graiet, M.: A correct by construction model for cbps systems verification. In: 2023 IEEE Symposium on Computers and Communications (ISCC). pp. 1299–1304 (2023). https://doi.org/10.1109/ISCC58397.2023.10217842
Toman, S.H., Lahouij, A., Kotel, S., Hamel, L., Toman, Z.H.,Graiet, M.: Service to service communication based on CBPS system: refinement and verification. Soft. Comput. 2024, 1–21 (2024)
A. Al Farooq, E.Al-Shaer,T.Moyer,and K. Kant,“IoTC2:A formal method approach for detecting conflicts in large scale iot systems”,In 2019IFIP/IEEE symposium on integrated network and service management(IM),pp 442-447,2019.
Shehata, M.; Eberlein, A.; Fapojuwo, A. Using semi-formal methods for detecting interactions among smart homes policies. Sci.Comput. Program. 2007, 67, 125–161. [CrossRef]
Shehata, M.; Eberlein, A.; Fapojuwo, A.O. A taxonomy for identifying requirement interactions in software systems. Comput.Netw. 2007, 51, 398–425. [CrossRef]
Hsu, K.H.; Chiang, Y.H.; Hsiao, H.C. Safechain: Securing trigger-action programming from attack chains. IEEE Trans. Inf.Forensics Secur. 2019, 14, 2607–2622. [CrossRef]
Ma, M.; Preum, S.M.; Stankovic, J.A. Cityguard: A watchdog for safety-aware conflict detection in smart cities. In Proceedings of the Second International Conference on Internet-of-Things Design and Implementation, Pittsburgh, PA, USA, 18–21 April 2017;pp. 259–270.
Liu, R.; Wang, Z.; Garcia, L.; Srivastava, M. RemedioT: Remedial actions for internet-of-things conflicts. In Proceedings of the 6th ACM International Conference on Systems for Energy-Efficient Buildings, Cities, and Transportation, New York, NY, USA, 13–14 November 2019 ; pp. 101–110.
Celik, Z.B.; Tan, G.; McDaniel, P.D. IoTGuard: Dynamic Enforcement of Security and Safety Policy in Commodity IoT; NDSS: San Diego,CA, USA, 2019.
Hoang,T.S.,“An introduction to the Event-B modelling method,” Industrial Deployment of System Engineering Methods,2013,pp.211-236.
M.Leuschel,and M.Butler,“ProB:A model checker for B,”In International symposium of formal methods europe(pp.855-874). Springer,Berlin,Heidelberg,2013.
Hallerstede, S.: On the purpose of Event-B proof obligations. In:Abstract State Machines, B and Z: First International Conference,ABZ 2008, London, UK, September 16-18, 2008, Proceedings 1,pp. 125–138. Springer (2008)
Abrial, J.R.: From z to b and then Event-B: assigning proofs to meaningful programs. In: Integrated Formal Methods: 10th International Conference, IFM 2013, Turku, Finland, June 10-14,2013, Proceedings 10, pp. 1–15. Springer (2013)
Abrial, J.: The B-book Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Leuschel M, Butler M (2013) ProB: A model checker for B.In: International symposium of formal methods Europe.Springer,Berlin, Heidelberg, pp 855–874
Muankid A, Ketcham M (2019) The real-time electrocardiogram signal monitoring system in wireless sensor network. Int J Online Biomed Eng 15(2)
Pradeep, P., & Kant, K. (2022). Conflict detection and resolution in IoT systems: a survey. IoT, 3(1), 191-218.
Huang, B., Dong, H., Bouguettaya, A.: Conflict detection in IoTbased smart homes. In: 2021 IEEE International Conference on Web Services (ICWS), pp. 303–313. IEEE (2021)
Jover, J., Bermúdez, A., & Casado, R. (2022). Priority-aware conflict resolution for U-space. Electronics, 11(8), 1225.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2026 Zinah Hussein Toman
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
