返回
Verifying Multi-vendor IoT Deployments Using Conditional Tables
DOI:10.1007/978-3-032-10554-7_8.png)
摘要
En 中文
近年来,物联网设备已在医疗保健、军事和家庭安全系统等关键环境中得到广泛部署。这些部署通常涉及非专业用户管理异构设备集合,增加了可能导致重大经济损失和物理损害的风险。不幸的是,此类部署面临独特挑战,如可见性不完整(例如需要与封闭软件系统互操作)、不兼容性(例如需要在不同协议和不同厂商创建的控制逻辑间交互)以及管理复杂性(例如需要以非专业用户可理解的方式表达复杂多样的意图)。尽管系统验证在其他领域对于早期发现错误至关重要,但这些挑战却阻碍了其在物联网中的应用。为在这些条件下执行验证,我们提出Pyotr系统,该系统基于数据库系统理论中的数学框架——称为不完全数据库。Pyotr能够整合异构设备数据,在故障和不确定知识条件下进行数据分析,使用易于使用的数据库风格查询验证预期行为,并提供一个通用的代数框架,以严谨且直观的方式对物联网系统进行推理。我们在大型物联网网络上的实验表明,Pyotr能够在几毫秒内可扩展地回答涉及数千个连接物联网设备的复杂查询。
Keyword:
Formal verification
IoT
Conditional Tables

