原文传递
基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究
| 论文题名： | 基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究 |
| 关键词： | 车站进路;计算机联锁;列车控制系统;形式化方法;多智能体系统;Event-B |
| 摘要： | 随着我国铁路事业的飞速发展，安全、高速成为铁路系统的硬性标准。我国在引进和借鉴欧洲ETCS列控系统的基础上，研发了拥有自主产权的CTCS-3级中国列车控制系统。计算机联锁系统则是保证列车行车安全的基础设备，主要是利用联锁软件完成联锁功能的一种安全苛求性系统，符合“故障-安全”原则。车站联锁控制直接关系到行车安全，也影响到车站作业的效率及行车组织工作，因此联锁系统在不断更新和改进。传统的联锁软件开发很多是用非形式化语言和自然语义来描述的，主要应用于软件工程的需求分析方法，在设计、分析和测试上已无法满足计算机联锁系统的安全需求。所以使用形式化的方法对联锁系统进行规范和说明，不仅可以提高计算机联锁软件的质量，也有利于进行更为严格的测试。 计算机联锁主要是由微型计算机的软件、硬件和一些电子、继电器件组成的，具有高可靠性和安全性的实时控制系统，联锁的意义就在于进路控制过程的表述。通过结合6502继电器的功能描述，对车站进路联锁控制逻辑进行完整说明，使用具有严谨数学语义的形式化方法对联锁系统的安全规范进行验证。 本文在学习和研究铁路联锁技术的基础上，以车站进路为场景，运用形式化方法Event-B和多智能体系统，阐述它们的特点和优点，并利用B方法的开发平台Rodin，对联锁系统安全性需求和控制功能进行建模和验证，并分别对车站进路的联锁逻辑进行描述，例如对车站进路中的信号、道岔、轨道区段、信号机等过程进行详细描述，把它们的特性和名称视为静态信息，把它们的变化状态视为动态信息，将信息存储到计算机存储器中，生成测试结果，分析结果以此来保证系统软件的一致性和完整性，提高软件的操作性能和安全属性。引入MAS概念，对联锁模型进行框架式的描述，建立不同场景下的Agent，通过对各个Agent的统一建模，最后形成MAS体系。文章实现了用形式化语言的建模过程，并生成证明义务。结果表明，对于车站联锁进路场景的复杂逻辑关系，采用形式化Event-B和MAS结合的方法，可以对模型进行有效规范化验证，不仅对形式化方法的发展有一定的参考价值，也对铁路联锁控制领域提供了切实有效的验证方法。 |
| 作者： | 韩佳芮 |
| 专业： | 计算机技术 |
| 导师： | 胡晓辉;张小冬 |
| 授予学位： | 硕士 |
| 授予学位单位： | 兰州交通大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
