论文部分内容阅读
在地下建筑智能化系统中，设备监控系统是基本的组成部分，其软件设计的正确性十分重要。提出了一种基于SPIN的地下建筑设备监控系统软件正确性验证方法。构建了基于iFIX组态软件的设备控制系统软件Promela模型，利用SPIN模型检验方法对其安全性进行了验证。还利用简化模型进行反例追踪，找出了安全性规约中存在的错误。检验结果表明提出的验证方法是有效性。