文档名：设备自动巡检控制逻辑的层级时间自动机建模与验证
地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠的运行,需对设备定期进行自动巡检在自动巡检过程中,设备自动巡检控制逻辑起到了举足轻重的作用为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(HFA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性及验证其正确性与可靠性现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性这种建模与形式化验证方法,弥补了之前无时间约束的漏洞,有效的确保了设备自动巡检控制逻辑的正确性与可靠性最终,该模型通过了模拟和验证,充分证明了设备自动巡检控制逻辑是正确可靠的.
作者：孙程 邢建春 杨启亮 韩德帅
作者单位：解放军理工大学国防工程学院南京210007解放军理工大学国防工程学院南京210007;计算机软件新技术国家重点实验室(南京大学)南京210093
母体文献：第十四届全国软件与应用学术会议论文集
会议名称：第十四届全国软件与应用学术会议
会议时间：2015年11月6日
会议地点：武汉
主办单位：中国计算机学会
语种：chi
分类号：
关键词：自动巡检 层级时间自动机 模型检测
在线出版日期：2017年7月25日
基金项目：
相似文献
相关博文
- 文件大小:
- 1.43 MB
- 下载次数:
- 60
-
高速下载
|
