设备自动巡检控制逻辑的层级时间自动机建模与验证

摘要：

地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠地运行,需对设备进行定期的自动巡检.在自动巡检的过程中,设备自动巡检控制逻辑起到了举足轻重的作用.为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(H FA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性,也未验证其正确性与可靠性.现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再利用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性.这种建模与形式化验证方法弥补了之前无时间约束的漏洞,有效确保了设备自动巡检控制逻辑的正确性与可靠性.最终,该模型通过了模拟和验证,这充分证明了设备自动巡检控制逻辑是正确可靠的.

关键词：自动巡检、层级时间自动机、UPPAAL、模型检测

所属期刊栏目：44

分类号：TP301(计算技术、计算机技术)

资助基金：江苏省自然科学基金BK20151451;装备预先研究基金9140A06050215JB25091;计算机软件新技术国家重点实验室南京大学开放课题KFKT2014B12

在线出版日期：2017-05-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：66-71,78