原文传递
车站信号计算机联锁逻辑关系形式化验证方法的研究
| 论文题名： | 车站信号计算机联锁逻辑关系形式化验证方法的研究 |
| 关键词： | 铁路运输;行车控制;铁路信号;计算机联锁 |
| 摘要： | 车站信号计算机联锁系统是铁路信号系统的重要组成部分，直接关系到车站行车作业的安全与效率，联锁软件是保障计算机联锁系统能正确执行联锁运算、实现联锁功能的关键组成部分，必须具备高安全性、高可靠性。随着高速铁路的快速发展，计算机联锁系统的应用场景变得越来越复杂，基于传统的联锁软件开发过程中存在的问题日益显露，例如:在需求定义上难以保证精确无歧义，仿真测试难以完整分析及验证软件安全性，容易形成安全隐患等。本文针对传统联锁软件开发过程中存在的问题，从6502电气集中联锁逻辑控制电路入手，提出基于有色Petri网(Colored Petri Net，CPN)的形式化解决方案，选取联锁系统的核心控制功能—进路控制，进行形式化建模和验证的探索研究。 本研究主要内容包括：⑴分析了当前广泛存在于联锁软件开发过程中的问题及引入形式化分析方法的优势及可行性，研究了基于CPN的形式化验证方法的理论基础和应用特点，介绍了CPN的建模、仿真、分析平台—CPN Tools，论证了采用层次CPN实现联锁逻辑关系形式化验证的可行性。⑵深入研究6502电气集中联锁控制电路，结合站场图，重点分析联锁进路控制过程中进路选排、进路锁闭、信号开放、进路正常解锁、进路非正常解锁等进路控制关键环节，抽象出关键环节的关键条件。⑶采用层次CPN由顶向下的开发方法为联锁进路控制建立顶层模型，由层次CPN的替代变迁引入进路选排、进路锁闭、信号开放、进路正常解锁、进路非正常解锁的子页模型，并对所建立的模型进行仿真，证明仿真过程中托肯的变化过程可很好的描述联锁进路控制过程，提出基于CPN的多条进路控制的形式化验证方法。⑷采用CPN Tools的状态空间分析工具，对所建立的模型进行状态空间分析，分析结果表明模型具有良好的安全性、正确性、完整性。⑸研究结果表明，基于CPN的形式化验证方法不仅能以动态的形式准确的描述联锁进路控制过程的功能需求，并且能完整的分析和验证模型的安全性，可用于联锁软件开发初期，对联锁逻辑关系进行验证分析，减少联锁软件的安全隐患。 |
| 作者： | 陶玲 |
| 专业： | 交通运输工程；交通信息工程及控制 |
| 导师： | 宋军 |
| 授予学位： | 硕士 |
| 授予学位单位： | 重庆交通大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
