标题：基于SPIN的地下建筑设备监控系统软件验证
作者：李亮 邢建春 杨启亮 孟祥朋
作者单位：解放军理工大学工程兵工程学院，江苏 南京 210007
关键字：监控系统，模型检验，SPIN，安全性
摘要：在地下建筑智能化系统中，设备监控系统是基本的组成部分，其软件设计的正确性十分重要。提出了一种基于SPIN的地下建筑设备监控系统软件正确性验证方法。构建了基于iFIX组态软件的设备控制系统软件Promela模型，利用SPIN模型检验方法对其安全性进行了验证。还利用简化模型进行反例追踪，找出了安全性规约中存在的错误。检验结果表明提出的验证方法是有效性。