形式化证明在区域控制器应用软件开发中的应用

形式化证明在区域控制器应用软件开发中的应用.pdf
区域控制器(ZC)是基于通信的列车自动控制(CBTC)信号系统中实现轨旁自动列车保护(ATP)功能的核心设备,用来计算列车移动授权以确保列车不发生冲撞,因此区域控制器软件实现的正确性对于确保整个CBTC信号系统的安全起着极其重要作用.采用形式化证明技术可以弥补传统开发过程中验证手段(如测试)片面性的缺点,是对软件(系统)全状态空间的正确性验证,确保软件(系统)实现与需求一致性.文章介绍了一种基于模型开发软件的形式化证明方法,描述了形式化证明工具、证明义务结构及形式化证明流程,并以iZC200型区域控制器应用软件为例,说明如何精确描述待证明安全属性,不同类型模型形式化证明及其优化方法.
作者：吕新军 罗勋 陈祥
作者单位：卡斯柯信号技术有限公司北京市地铁运营有限公司地铁运营技术研发中心
母体文献：2016年全国智慧城市与轨道交通学术会议论文集
会议名称：2016年全国智慧城市与轨道交通学术会议  
会议时间：2016年4月19日
会议地点：苏州
主办单位：中国城市科学研究会数字城市专业委员会
语种：chi
分类号：TP3U49
关键词：地下铁路  区域控制器  软件开发  形式化证明技术
在线出版日期：2016年6月21日
基金项目：
相似文献
相关博文

2024-12-7 22:11 上传 形式化证明在区域控制器应用软件开发中的应用.pdf

文件大小:

1.34 MB

下载次数:

60

高速下载