原文传递
基于CSP的城轨CBTC联锁逻辑形式化建模与验证
| 论文题名： | 基于CSP的城轨CBTC联锁逻辑形式化建模与验证 |
| 关键词： | 列车控制;联锁系统;形式化语言;通信顺序进程;线性时序逻辑;ProB |
| 摘要： | 随着通信技术、计算机技术、自动控制技术的发展，基于通信的列车控制（Communication Based Train Control，CBTC）逐渐成为城市轨道交通信号系统的首选方案。作为CBTC系统的一个子系统，联锁系统主要实现进路控制、区间临时限速、扣车和取消、站台紧急关闭和取消等功能，其安全性和可靠性对列车能否安全高效运行有很大影响。联锁逻辑作为联锁软件的核心，其正确性不论是对联锁系统的开发还是测试都十分重要。 本文从计算机联锁系统入手，首先分析并总结了CBTC联锁系统的功能性需求和安全性需求。其中对联锁逻辑的描述大部分还是依靠自然语言，鉴于自然语言不够规范并且容易有歧义，具有严格定义的数学基础和推理规则的形式化方法已经在轨道交通控制系统中有了一定的研究基础。 本文通过对经典的形式化方法的比较，给出了一种基于通信顺序进程(Communicational Sequential Processes，CSP)对城轨CBTC联锁逻辑进行描述的方法。联锁表是说明受控信号设备之间联锁关系的图表，是联锁逻辑的体现。因此本文利用形式化语言CSP描述联锁表所表达的逻辑关系，把每条进路分别看做一个进程，那么每个进程内部都是调度员、道岔、信号机和轨道区段与联锁设备相互通信、交互作业的过程，则整个联锁表就是各个进路的行为的并发组合。然后用CSP验证工具ProB结合线性时序逻辑，通过行为动画、模型检测、一致性验证等方法来验证模型是否满足功能性要求和安全性要求，进而来证明联锁表所描述的联锁逻辑的正确性。 文章的最后把这种基于CSP的形式化方法应用于北京地铁亦庄线同济南站，对该站的联锁表进行建模和验证，证明了该方法的可行性及正确性。 |
| 作者： | 马慧 |
| 专业： | 控制工程 |
| 导师： | 黄友能 |
| 授予学位： | 硕士 |
| 授予学位单位： | 北京交通大学 |
| 学位年度： | 2013 |
| 正文语种： | 中文 |
检索历史
应用推荐
