IoTC2：一种用于检测大规模物联网系统中冲突的形式化方法
密码学与安全
2018-12-11 v1 计算机与社会
摘要
物联网（IoT）已成为医疗、交通基础设施、智能家居、智能购物与电子商务等不同领域的通用范式。凭借其互操作功能，现在可将物联网各领域连接起来，为用户提供高效服务。由于大量物联网设备可同时连接与通信，可能出现触发对执行器或环境特征的冲突动作之事件。然而，利用形式化方法检测物联网系统中冲突情形的研究工作极少。本文提供一种形式化方法途径——IoT 冲突检测器（IoTC2），以针对冲突确保控制器与执行器行为的安全性。任何策略违例均导致冲突被检测出来。我们定义了控制器、动作与触发事件的安全策略，并用 Prolog 实现以证明其逻辑完备性与可靠性。此外，我们在 Matlab Simulink 环境中利用其内置的模型验证模块实现了检测策略。我们在 Simulink 中创建智能家居环境，并展示冲突如何影响动作及相应特征。我们还在仿真环境中实验了所提方法的可扩展性、效率与准确性。
引用
@article{arxiv.1812.03966,
title = {IoTC2: A Formal Method Approach for Detecting Conflicts in Large Scale IoT Systems},
author = {Abdullah Al Farooq and Ehab Al-Shaer and Thomas Moyer and Krishna Kant},
journal= {arXiv preprint arXiv:1812.03966},
year = {2018}
}