IoTC2: A Formal Method Approach for Detecting Conflicts in Large Scale IoT Systems

TL;DR

This paper introduces IoTC2, a formal method-based tool for detecting conflicts in large-scale IoT systems, ensuring safety and correct behavior of controllers and actuators through logical verification and simulation.

Contribution

It presents a novel formal method approach combining Prolog and Simulink to detect conflicts in IoT systems, addressing a gap in existing research.

Findings

Effective conflict detection in simulated smart home environment

Demonstrated scalability and efficiency of IoTC2

Validated accuracy of conflict detection policies

Abstract

Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart home, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together for providing competent services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions to an actuator or an environmental feature. However, there have been very few research efforts made to detect conflicting situation in IoT system using formal method. This paper provides a formal method approach, IoT Confict Checker (IoTC2), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We defined the safety policies for controller, actions, and triggering events and implemented the those with Prolog to prove the logical completeness and soundness. In addition to that, we have implemented the detection policies in Matlab Simulink Environment with its built-in Model Verification blocks. We created smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. We have also experimented the scalability, efficiency, and accuracy of our method in the simulated environment.