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