基于eventb的联锁系统进路控制建模与验证研究

《基于eventb的联锁系统进路控制建模与验证研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、劣蠊交硕士学位论文基于Event．B的联锁系统进路控制建模与验证研究ResearchonEvent—-BBasedModelingandVerificationofInterlockingRouteControl作者：童湖东导师：宁滨北京交通大学2013年3月学位论文版权使用授权扩I堕IIIIIIIIIIIIllliiiii塑miilliiliPil吵iiiIPrJiiillilliil本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同

2、意学校向国家有关部门或机构送交论文的复印件和磁盘。(保密的学位论文在解密后适用本授权说明)学位论文作者签名：刍浦琢签字日期：阳弓年夕月日中图分类号：U284．37UDC：625学校代码：10004密级：公开北京交通大学硕士学位论文基于Event—B的联锁系统进路控制建模与验证研究ResearchonEvent—BBasedModelingandVerificationofInterlockingRouteContr01作者姓名：童湖东导师姓名：宁滨学位类别：工学学科专业：交通信息工程及控制学号：10120315职称：教授学位级别：硕士研究方向：基于通信的列车运行控制还仃弪制北京交

3、通大学2013年3月致谢本论文的工作是在我的导师宁滨教授的悉心指导下完成的，宁滨教授严谨的治学态度和科学的工作方法给了我极大的帮助和影响。在此衷心感谢三年来宁滨老师对我的关心和指导。王海峰副教授悉心指导我们完成了实验室的科研工作，在学习上和生活上都给予了我很大的关心和帮助，在此向王海峰老师表示衷心的谢意。感谢荀径、李伟、李雷、张路、张宏韬、边远、蒋琦、曹欣师兄和周宁、张越、汤永、吴雅静等同学在实验室工作期间给与我的热情帮助。感谢我的父母，他们的理解和支持使我能够在学校专心完成我的学业，在人生道路上保持前行的勇气和动力。中文摘要摘要：联锁系统是铁路信号系统的重要组成部分，直接关系到

4、车站行车和作业的安全与效率。计算机联锁系统由于具有高效、智能化、易于维护的优点而成为当前联锁系统运用的主流。联锁软件是计算机联锁系统正确执行联锁运算、实现联锁功能的关键，必须具备极高的安全性和可靠性。当前的联锁软件开发主要使用传统的基于软件工程的方法，在需求定义上难以保证完备性和一致性，仿真和测试也不足以完整分析和验证软件安全性，容易形成安全隐患，同时，开发出的软件可维护性不高。本文针对传统联锁软件开发方法存在的问题，从实际应用角度出发提出基于Event．B的形式化解决方案，选取联锁软件核心功能——进路控制进行了形式化建模和验证的探索研究，主要研究工作如下：(1)分析了当前联软件

5、开发方法存在的缺陷和引入形式化解决方案的可能性，研究了Event-B形式化建模验证方法的理论基础和应用特点，介绍了Event-B方法相关工具，提出了基于Event．B的联锁软件形式化开发方法。(2)分析了联锁软件进路控制具体流程，在此基础上制定了联锁进路控制Event．B模型的建立步骤和精化策略，并根据制定的步骤和精化策略，在Rodin工具平台下借助UML．B工具逐步建立了包含进路选排、信号控制、进路锁闭、自动解锁和人工解锁各进程功能需求和安全需求的进路控制Event．B模型。(3)采用模型仿真和模型证明相结合的方法对建立的联锁进路控制Event．B模型进行了形式化验证，其中模型

6、仿真部分采用了UML．B状态机仿真的方法，模型证明部分则借助Event．B证明义务机制和Rodin平台采用了自动证明和交互式证明相结合的方法，结果表明本文所建立的进路控制模型能覆盖系统功能需求和安全需求，模型有效性、正确性和一致性能得到完整验证。本文的研究结果表明，基于Event．B的形式化建模验证方法能准确和有效的描述联锁进路控制的功能需求和安全需求，并且完整的分析和验证模型安全特性，能运用于联锁软件开发中以增强软件安全性并提高开发效率。关键词：联锁软件；进路控制；形式化方法；Event．B分类号：U284．37ABSTRACTABSTRACT：Asanimportantpar

7、tofrailwaysignalsystem，interlockingsystemplaysakeyroleinensuringthesafetyoftrainrunninginstationandimprovingefficiency．Computerbasedinterlockingisnowthemaindirectionofinterlockingsystemdevelopmentforitsadvantagesofhighefficiency,intelligencea