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

摘要

Internet of Things (IoT) has become a common paradigm for different domains such as health care, transportation infrastructure, smart homes, smart shopping, and e-commerce. With its interoperable functionality, it is now possible to connect all domains of IoT together to provide comprehensive services to the users. Because numerous IoT devices can connect and communicate at the same time, there can be events that trigger conflicting actions for an actuator or an environmental feature. This paper provides a formal method approach, IoT Confict Checker (IoTC²), to ensure safety of controller and actuators' behavior with respect to conflicts. Any policy violation results in detection of the conflicts. We define the safety policies for controller, actions, and triggering events and implement them in 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 a smart home environment in Simulink and showed how the conflicts affect actions and corresponding features. The scalability, efficiency, and accuracy of our method are tested in this simulated environment.