物联网(Internet Of Things,Io T)如今已深入到个人生活和工业生产的各个方面,智能设备大量出现在家庭生活中,为用户带来舒适和便利。然而由于智能家居系统复杂多变,用户缺乏专业知识等原因,所面临的安全挑战也越来越严峻。智能家居系统与用户的隐私、财产和生命安全息息相关,如何保证其安全性成为相关领域的重要研究课题。模型检验技术是近年来事件驱动物联网系统安全验证中被广泛使用的技术之一。该技术对复杂系统建立状态迁移模型来描述系统行为,通过自动遍历系统模型的有限状态空间来验证系统是否满足某些性质。然而在对真实Io T系统进行验证时,模型检验技术仍然面临一些问题。第一,Io T系统由各种设备组成,对设备准确建模决定了验证结果的可信度。目前设备模型的获取采用人工建模或源码分析的方法,这些方法得到的模型大多与真实设备有差异,很少有研究工作考虑从设备的自然语言文本描述中获取模型。第二,模型检验技术采用形式化规约来描述系统性质,最常用是线性时序逻辑(Linear Temporal Logic,LTL)。但普通用户不具备专业的数理知识,无法理解或提供形式化规约,他们通常使用自然语言来表达需求。这些问题极大地限制了现有验证工具在真实Io T系统上的应用。针对以上两个问题,本文从以下方面展开系统研究:··针对设备建模问题,本文提出了一种基于IFTTT功能描述自然语言处理的设备辅助建模方法。该方法首先利用自然语言处理技术对设备功能描述语句进行分析,抽取出每个句子的语义信息。然后利用词向量技术和语义词典,针对功能描述的特点设计了功能相关性评估策略,通过对功能描述聚类分析,得到不同的功能类。在此基础上提出了从功能类中抽取出不同模型元素的方法,构造初始模型。·针对形式化规约的获取问题,本文提出了一种基于领域知识的自然语言到LTL规约的自动生成方法。该方法首先对自然语言规约进行解析,然后从语法树中识别关键节点,抽取出相应的语义信息和时序逻辑信息,生成树形中间表示形式。最后利用模板将所有子句转换成原子命题,并提出一种基于深度优先搜索的算法,将原子命题与时序操作符、逻辑操作符结合,由树结构生成LTL规约。针对自然语言的结构歧义问题,本文提出了一种基于领域知识的结构歧义消除方法,能够自动检测并修正语法树中的结构歧义。·本文实现了设备辅助建模工具和LTL规约生成工具。为了验证工具在真实数据集上的执行效果,本文实施了一项调研工作,收集用户给出的规则和自然语言规约。本文在IFTTT功能描述集和自然语言规约数据集上展开评估实验,并将生成的模型和LTL规约用于验证真实用户构建的智能场景。实验结果显示,我们的工具在正确率和效率上都有很好的表现,而且生成的模型和LTL规约能够有效地帮助用户发现智能家居场景中的错误。