车站信号计算机联锁逻辑关系形式化验证方法的研究

《车站信号计算机联锁逻辑关系形式化验证方法的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号U284.3单位代码10618密级学号2120112002硕士学位论文车站信号计算机联锁逻辑关系形式化验证方法的研究研究生姓名：陶玲导师姓名及职称：宋军教授申请学位类别工学硕士学位授予单位重庆交通大学一级学科名称交通运输工程论文提交日期2015年4月25日二级学科名称交通信息工程及控制论文答辩日期2015年6月4日2015年6月10日TheStudyofFormalVerificationMethodaboutRailSignalInterlockingLogicRelationADissertationSubmittedfort

2、heDegreeofMasterCandidate：TaoLingSupervisor：Prof.SongJunChongqingJiaotongUniversity,Chongqing,China重庆交通大学学位论文原创牲声明？本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究．．工作所取得的成果？除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均己在文中Ｗ明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文

3、作者签名；曰期：＞心年月又曰重庆交通大学学位论文化权使巧授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校化。留并向国家有关部口或机构送交论文的复印件和电子版，允许论文被查阀和借阅本人授权重庆交通大学可Ｗ将本学位论文的全部内容编入有关数据库进行检索，、。同时授权中国科可＞缩印或扫描等复制手段保存和汇编本学位论文１＾采用影印学技术信息研究所将本人学位论文收录到《中国学位论文全文数据库》，并进行信息服务、复制、发斤、信息哟络传播等），同时本人保留（包括但不限于汇编在其他媒体发表论文的权利

4、。学位论文作者签名：＾指导教师签名：＾曰新：＞化年＾月方曰曰期啤月曰６若；本人同意将本学位论文提交至中国学术期刊（光蟲版）电子杂志社ＣＮＫＩ系列数据库中全文发布，并按《中国优秀博硕壬学位论文全文数据库出版章程》规定孚受相关权益。、学位论文作者签名：指导教师齡：＾日期：）。社年＾月？日日期：庐月＾日摘要车站信号计算机联锁系统是铁路信号系统的重要组成部分，直接关系到车站行车作业的安全与效率，联锁软件是保障计算机联锁系统能正确执行联锁运算、实现联锁功能的关键组成部分，必须具备高安全性、高可靠性。随着高

5、速铁路的快速发展，计算机联锁系统的应用场景变得越来越复杂，基于传统的联锁软件开发过程中存在的问题日益显露，例如：在需求定义上难以保证精确无歧义，仿真测试难以完整分析及验证软件安全性，容易形成安全隐患等。本文针对传统联锁软件开发过程中存在的问题，从6502电气集中联锁逻辑控制电路入手，提出基于有色Petri网（ColoredPetriNet，CPN）的形式化解决方案，选取联锁系统的核心控制功能—进路控制，进行形式化建模和验证的探索研究，主要研究工作如下：（1）分析了当前广泛存在于联锁软件开发过程中的问题及引入形式化分析方法的优势及可行性，

6、研究了基于CPN的形式化验证方法的理论基础和应用特点，介绍了CPN的建模、仿真、分析平台—CPNTools，论证了采用层次CPN实现联锁逻辑关系形式化验证的可行性。（2）深入研究6502电气集中联锁控制电路，结合站场图，重点分析联锁进路控制过程中进路选排、进路锁闭、信号开放、进路正常解锁、进路非正常解锁等进路控制关键环节，抽象出关键环节的关键条件。（3）采用层次CPN由顶向下的开发方法为联锁进路控制建立顶层模型，由层次CPN的替代变迁引入进路选排、进路锁闭、信号开放、进路正常解锁、进路非正常解锁的子页模型，并对所建立的模型进行仿真，证明

7、仿真过程中托肯的变化过程可很好的描述联锁进路控制过程，提出基于CPN的多条进路控制的形式化验证方法。（4）采用CPNTools的状态空间分析工具，对所建立的模型进行状态空间分析，分析结果表明模型具有良好的安全性、正确性、完整性。本文研究结果表明，基于CPN的形式化验证方法不仅能以动态的形式准确的描述联锁进路控制过程的功能需求，并且能完整的分析和验证模型的安全性，可用于联锁软件开发初期，对联锁逻辑关系进行验证分析，减少联锁软件的安全隐患。关键词：联锁；进路控制；形式化方法；CPN；CPNToolsIABSTRACTAsanimportan

8、tpartofrailwaysignalsystem,interlockingsystemplaysandirectlyroleinthesafetyandefficiencyofstationoperat