该论文提出了一种新颖的形式化威胁分析器，专门针对基于活动监测的智能家居供暖、通风和空调（HVAC）控制系统。研究背景在于智能家居系统日益普及，但HVAC控制系统中集成的活动监测功能可能引入安全漏洞，攻击者可利用这些漏洞进行隐私侵犯或物理控制干扰。论文的核心方法是构建一个形式化模型，将HVAC系统的行为、用户活动模式以及潜在威胁场景抽象为数学规范，并利用模型检测技术自动验证系统是否存在特定类型的安全威胁。主要贡献包括：设计了一个通用的威胁建模框架，能够捕获基于活动监测的HVAC系统的独特攻击面；开发了自动化分析工具，可输出可解释的风险报告；通过真实场景的案例研究验证了分析器的有效性，证明了其能够发现常规安全审计难以识别的隐蔽威胁。实验表明，该分析器在检测物联网环境中的信息泄露和物理篡改攻击方面具有较高准确性。该研究适合智能家居安全研究人员、HVAC系统设计师以及物联网安全从业者阅读。