形式化方法是建立在严密数学逻辑基础上的系统研究方法,其严谨、精确的特性适合发现系统设计与开发过程中并发性、安全性等方面的问题。PAT(Process Analysis Toolkit)平台是功能较为全面、易于使用的形式化建模与自动检验工具,已成功对特定的智能家居复合行为进行建模和验证,发现和改善了智能家居系统中的潜在错误和不足,但还未形成智能家居系统形式化验证的描述和验证一般模型。智能家居平台是指将智能设备、控制程序、操作系统等复合成为用户提供服务的综合系统,其设备异构性与安全重要性对平台的运行正确性、安全性等提出了严苛的要求,如何高效检测运行规则异常和安全缺陷也成为亟待解决的问题。针对以上问题,本文提出一种描述智能家居平台的形式化模型,通过对平台整体及各模块的形式化建模,用PAT工具对系统的功能和相关特性进行验证,发现潜在的异常与冲突,为改进系统提供依据。实验表明该模型能够有效地对智能家居平台进行特性模拟,并结合PAT平台对系统进行检验。本文主要内容包括以下几个部分:分析智能家居平台构成中的各组成部分(控制程序、设备控制框架、通用数据库、智能设备),明确其功能和结构特性以及通信控制方法,提出智能家居平台架构模型;结合实际应用中平台所应具备的性质,确定系统需求。给出智能家居平台模型的形式化定义,实现对智能家居平台的模型描述,包括平台各模块及其并行通信的模型描述。结合应用场景对系统需求进行说明,明确智能家居平台所需检验的相关特性,并使用形式化语言对特性进行准确描述。在PAT平台上对智能家居平台模型进行形式化检验,实验包括对平台对象和平台运行过程两方面的检验与改进,实验表明,借助于PAT工具可以高效地对智能家居平台进行正确性和实用性的验证。