随着现代信息技术的不断发展,物联网已经进入各个领域,并得到了广泛应用,其中,智能家居物联网也得到了快速发展并走进了千家万户。以IFTTT框架为代表的事件驱动型物联网系统控制框架使得智能家居更加智能、更加个性化,用户通过编写规则就可以简单而高效地构建自己的智能家居系统。但是,这一普遍使用的机制背后存在严峻的安全问题。普通用户通常对其给出规则的行为缺乏完整理解,随着系统规则数目增长,用户的理解与把握能力快速下降。如何保证用户设计的智能家居场景能够按照用户期望运行,不会出现意外的安全问题,如何判断智能家居系统在各种情况下的安全性,这些基本问题普通用户难以回答。因此,帮助用户实现对事件驱动型智能家居物联网系统进行安全检验是一项十分重要的工作。本文提出了一种面向事件驱动型智能家居物联网系统的自动化建模和安全检验方法。该方法综合考虑智能家居系统安全相关因素,对智能家居系统进行自动化建模,使用模型检验和模糊测试方法进行模型驱动的系统验证和测试,实现对系统的安全检验。本文的主要工作如下:●针对事件驱动型智能家居系统设计了一套自动化建模与安全验证方法。本文针对用户自定义的事件驱动型智能家居系统,使用有限状态机(Finite State Machine,FSM)进行系统建模,模型中综合考虑智能家居系统安全相关因素,并给出可自动化生成的安全性质规约,完成对事件驱动型智能家居系统安全性验证的模型检验工作。●基于事件驱动型智能家居系统模型,应用模糊测试思想实现对系统模型的安全性测试。本文提出了一种对系统模型进行安全检验的模糊测试方法,该方法定义模型输入向量,在系统模型状态空间内生成对应的状态路径,基于给定规约对状态路径进行验证,在系统模型中寻找规约的反例路径。为实现更优的状态路径探索,本文提出了一种距离度量方式来衡量模型输入向量优劣,从而实现模型输入向量的选择和变异,优化测试方案。●实现了一个面向用户的事件驱动型智能家居系统自动化安全检验平台——门神。门神提供直观的系统配置和安全检验功能,帮助用户快速上手实现对智能家居系统的安全检验工作。本文从两个方面进行了实验数据的收集工作,并基于收集到的数据进行系统验证和测试实验,实验结果显示本文方法在发现问题和系统检验效率上都有较好的表现。