IoTC2: A Formal Method Approach for Detecting Conflicts in Large Scale IoT Systems
IoTC2: A Formal Method Approach for Detecting Conflicts in Large Scale IoT Systems
复制标题
DOI：
--
复制
发表时间：
2018-12
期刊：
影响因子：
--
通讯作者：
A. Farooq;E. Al-Shaer;Thomas Moyer;K. Kant
中科院分区：
文献类型：
--
作者：
A. Farooq;E. Al-Shaer;Thomas Moyer;K. Kant
物联网（IoT）已成为医疗保健、交通基础设施、智能家居、智能购物和电子商务等不同领域的常见范例。凭借其可互操作的功能，现在可以将物联网的所有领域连接在一起，为用户提供全面的服务。由于许多物联网设备可以同时连接和通信，因此可能会发生触发致动器或环境特征的冲突动作的事件。本文提供了一种形式化的方法，物联网冲突管理（IoTC 2），以确保控制器和执行器的行为相对于冲突的安全。任何违反策略的行为都会导致检测到冲突。我们定义了控制器、动作和触发事件的安全策略，并在Prolog中实现，以证明逻辑的完整性和可靠性。除此之外，我们还在Matlab Simulink环境中使用其内置的模型验证模块实现了检测策略。我们在Simulink中创建了一个智能家居环境，并展示了冲突如何影响动作和相应的功能。我们的方法的可扩展性，效率和准确性进行了测试，在这个模拟环境。
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 (IoTC2), 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.