<p>In the rapidly expanding Internet of Things (IoT) field, it is imperative to guarantee the accuracy and dependability of system behaviours. IoT systems frequently encounter obstacles associated with conflicting rules, which can result in erroneous operations and potential system failures. The fast deployment of IoT systems increases the number of conflicts that arise as a result of different interactions of the service rules among IoT systems. These rules share the same physical environment and are controlled by various entities or organisations. Conflict management has become a significant issue as a result of the extensive implementation of these systems. This paper introduces an innovative way to detect the conflict rules in IoT systems by employing the Event-B formal method. Through the development of formal models of the IoT system and the utilisation of abstract and refinement techniques, any conflicts are methodically detected and addressed. The purpose of this paper is to argue for the utilisation of Event-B formal modelling and verification throughout the first phases of IoT system development in order to find and repair faults as quickly as possible. The suggested model accounts for different kinds of conflicts, including: oppositional conflict, duration conflict, numeric conflict, dependency conflict, shadow conflict, and semantic conflict. The Rodin platform is employed to automate the verification process, guaranteeing that all defined invariants and attributes are maintained during the functioning of the system. In order to demonstrate the efficacy of our suggested model, we provide motivational examples of service rules that involve the use of smart home systems. The model effectively detects potential conflicts that may occur in these types of situations. We exhibit that it is possible to guarantee conflict strategy accuracy by utilising the Rodin platform and ProB, which gives users a degree of assurance regarding the resilience of IoT deployments.</p>