基于csp城轨cbtc联锁逻辑形式化建模和验证论文

《基于csp城轨cbtc联锁逻辑形式化建模和验证论文》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学位论文版权使用授权书嬲本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索，提供阅览服务，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关部门或机构送交论文的复印件和磁盘。(保密的学位论文在解密后适用本授权说明)学位论文作者签名：与慧翩躲童友键签字日期：压，；年7月2Et签字日期：2吖弓年7月2日>中图分类号：U284．3UDC：625学校代码：10004密级：公开北京交通大学专业硕士

2、学位论文基于CSP的城轨CBTC联锁逻辑形式化建模与验证FormalModelingandVerificationofUrbanRailCBTCInterlockingBasedonCSP作者姓名：马慧导师姓名：黄友能工程领域：控制工程北京交通大学2013年6月学号：11125075职称：副教授学位级别：硕士致谢本论文是在我的导师黄友能老师的精心指导下完成的，从论文的选题到最终定稿都凝聚了导师的智慧和心血。两年来黄老师在学习和生活上给予了我悉心指导和无私帮助，他严谨的治学态度和科学的工作方法将使

3、我受益终生。在此，谨向我的导师黄友能副教授致以最诚挚，最衷心的感谢。感谢徐田华老师、吕继东老师和赵林老师在我的论文选题、研究工作及学习形式化方法中给予的莫大帮助。感谢实验室赵训婷师姐、朱葛等同学在平时的学习生活中给予我的帮助，与你们共同学习，共同进步的过程使我受益匪浅。感谢我的家人，是你们一贯的支持和爱护才使我得以顺利完成学业。感谢在百忙之中对我的论文进行评阅和指导的各位专家，学者。最后，衷心感谢所有曾经帮助过我的老师、同学和朋友们，祝愿每一个人健康幸福。中文摘要摘要：随着通信技术、计算机技术、

4、自动控制技术的发展，基于通信的列车控制(CommunicationBasedTrainControl，CBTC)逐渐成为城市轨道交通信号系统的首选方案。作为CBTC系统的一个子系统，联锁系统主要实现进路控制、区间临时限速、扣车和取消、站台紧急关闭和取消等功能，其安全性和可靠性对列车能否安全高效运行有很大影响。联锁逻辑作为联锁软件的核心，其正确性不论是对联锁系统的开发还是测试都十分重要。本文从计算机联锁系统入手，首先分析并总结了CBTC联锁系统的功能性需求和安全性需求。其中对联锁逻辑的描述大部分还

5、是依靠自然语言，鉴于自然语言不够规范并且容易有歧义，具有严格定义的数学基础和推理规则的形式化方法己经在轨道交通控制系统中有了一定的研究基础。本文通过对经典的形式化方法的比较，给出了一种基于通信顺序进程(CommunicationalSequentialProcesses，CSP)对城轨CBTC联锁逻辑进行描述的方法。联锁表是说明受控信号设备之间联锁关系的图表，是联锁逻辑的体现。因此本文利用形式化语言CSP描述联锁表所表达的逻辑关系，把每条进路分别看做一个进程，那么每个进程内部都是调度员、道岔、信

6、号机和轨道区段与联锁设备相互通信、交互作业的过程，则整个联锁表就是各个进路的行为的并发组合。然后用CSP验证工具ProB结合线性时序逻辑，通过行为动画、模型检测、一致性验证等方法来验证模型是否满足功能性要求和安全性要求，进而来证明联锁表所描述的联锁逻辑的正确性。文章的最后把这种基于CSP的形式化方法应用于北京地铁亦庄线同济南站，对该站的联锁表进行建模和验证，证明了该方法的可行性及正确性。关键词：基于通信的列车控制；联锁；形式化方法：通信顺序进程；线性时序逻辑；ProB分类号：U284．3ABST

7、RACTABSTRACT：Withthedevelopmentofcommunicationtechnology，computertechnologyandautomaticcontroltechnology，communicationbasedtraincontroltechnologyhasgraduallybecomethepreferredsolutionforurbantransportationsystem．AsapartoftheCBTCsystem，theinterlocking

8、systemeffectsonthesafetyandspeedofmetrain，achievesmanyfunctionsuchasroutecontrol，signalcontrol，intervaltemporaryspeedlimitation，platformhold，trainhold，ESAandSOon．Interlockingcontrollogicisthecoreoftheinterlockingsoftware，itscorrectnessisimportantnoto