基于event-b和mas的车站进路联锁控制逻辑的形式化方法研究

《基于event-b和mas的车站进路联锁控制逻辑的形式化方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、＇Ｉｆ．．．１；Ｉ＇＇Ｉ＇‘，‘＜＇＇．＜中图分类号：ＴＰ３９１密公开ＵＤＣ：本校编号；邀Ｗ交遺乂＃工程硕±学位论文ｎ－论文题目基于ＢｖｅｔＢ和Ｍ乂５的车站进路；联铺把制還辑的形式化方法研寐研究生姓名：韩佳巧学号；０６１２１１１学校指导教师姓名；胡晓辉职称：教授企业指导教师姓名：张小冬职称：高工：计算机技术申请学位工程领域名称论文提交日期：２０１５．４．９论文答辩日期２０１５．５．３１；＿独创性声明本人声明所呈交的学位论文是本

2、人在导师指导下进行的研巧工作和取得的研究成果，除了文中特别加标注和致谢么处外，论文中不包含其他人已经发表或撰写过的研巧成果，也不包含获得兰州交通大学或其他教育机构的学位或证书而使用过的材料…同工作的同志对本研究所做的任何贡献均己在论文中作。与我了明确的说明并表示了谢意。学位论文作者签名：＾隹＾＾签字日期《年＾月侣日学位论文版权使用授权书本学位论文作者完全了解兰州巧通大学有关保留、使用学位论文的规定。１特授权兰州交通大学可＾＞将学位论文的全部或部分内容编入有关数据库进行检、索，并采用影印缩印或扫描等复制手段保存、汇编ｔｕ

3、供查阅和借阅。同意学校向国家有关部口或机构送交论文的复印件和磁盘。（保密的学位论文在解密后适用本授权说明）学位论文作者签名：蘇隹巧导师签名：签字日期：支。／５年《月＇多日签字日期；从／许《月文日＾工程硕士学位论文基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究TheResearchontheFormalMethodsoftheStationInterlockControlLogicBasedonEvent-BandMAS作者姓名：韩佳芮工程领域：计算机技术学号：0612111校内导师：胡晓辉企业导师：张小冬完成日期

4、：2015年4月9日兰州交通大学LanzhouJiaotongUniversity兰州交通大学工程硕士学位论文摘要随着我国铁路事业的飞速发展，安全、高速成为铁路系统的硬性标准。我国在引进和借鉴欧洲ETCS列控系统的基础上，研发了拥有自主产权的CTCS-3级中国列车控制系统。计算机联锁系统则是保证列车行车安全的基础设备，主要是利用联锁软件完成联锁功能的一种安全苛求性系统，符合“故障-安全”原则。车站联锁控制直接关系到行车安全，也影响到车站作业的效率及行车组织工作，因此联锁系统在不断更新和改进。传统的联锁软件开发很多是用非形式化语言和自然语义来描述的，主要应用

5、于软件工程的需求分析方法，在设计、分析和测试上已无法满足计算机联锁系统的安全需求。所以使用形式化的方法对联锁系统进行规范和说明，不仅可以提高计算机联锁软件的质量，也有利于进行更为严格的测试。计算机联锁主要是由微型计算机的软件、硬件和一些电子、继电器件组成的，具有高可靠性和安全性的实时控制系统，联锁的意义就在于进路控制过程的表述。通过结合6502继电器的功能描述，对车站进路联锁控制逻辑进行完整说明，使用具有严谨数学语义的形式化方法对联锁系统的安全规范进行验证。本文在学习和研究铁路联锁技术的基础上，以车站进路为场景，运用形式化方法Event-B和多智能体系统，

6、阐述它们的特点和优点，并利用B方法的开发平台Rodin，对联锁系统安全性需求和控制功能进行建模和验证，并分别对车站进路的联锁逻辑进行描述，例如对车站进路中的信号、道岔、轨道区段、信号机等过程进行详细描述，把它们的特性和名称视为静态信息，把它们的变化状态视为动态信息，将信息存储到计算机存储器中，生成测试结果，分析结果以此来保证系统软件的一致性和完整性，提高软件的操作性能和安全属性。引入MAS概念，对联锁模型进行框架式的描述，建立不同场景下的Agent，通过对各个Agent的统一建模，最后形成MAS体系。文章实现了用形式化语言的建模过程，并生成证明义务。结果表

7、明，对于车站联锁进路场景的复杂逻辑关系，采用形式化Event-B和MAS结合的方法，可以对模型进行有效规范化验证，不仅对形式化方法的发展有一定的参考价值，也对铁路联锁控制领域提供了切实有效的验证方法。关键词：联锁；形式化方法；Event-B；多智能体系统；继电器论文类型：应用研究-I-基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究AbstractWiththerapiddevelopmentofChina’srailway,theconceptsofsafeandhighspeedhavebeenregardedasthecorestan

8、dardofrailwaysystem.BasedonEurope