文档介绍：博士学位论文列车运行控制系统分层形式化建模与验证分析作者:吕继东导师:唐涛教授北京交通大学⒊年
办毋学位论文作者签名:盔膏,签字日期:辍隆日签字日期:年耭日导师签名:
防鴉.—卜衄列车运行控制系统分层形式化建模与验证分析作者姓名:吕继东导师姓名:唐涛学位类别:工学职称:教授学位级别:博士学科专业:交通信息工程及控制研究方向:高速列车运北京交通大学年学号:踟.、、,仃
最终成稿都倾注了导师的智慧和心血。五年来唐老师在学习和生活中给予了悉心指导和无私帮助,唐老师渊博的学识、严谨的治学态度、敏锐的科学思维和富有启发性的分析将使我受益终生。在此,谨向我的导师唐涛教授致以最诚挚、最衷心的感谢。感谢轨道交通控制与安全国家重点实验室郜春海、李开成、刘波、王海峰、黄有能、刘中田、蔡伯根等老师以及列控系统规范验证小组的徐田华、赵林等老师,感谢这些老师在科研工作中的支持和生活上的帮助。感谢程荫杭、蔡伯根、赵会兵、宋永端教授对我论文的选题和研究工作提出的宝贵意见。感谢实验室周达天、燕飞、郭宝清老师在博士学习期间给予的帮助和指导,感谢牛儒、曹源、陈磊、苟径等各位博士在课题研究和论文写作过程中给予我莫大的帮助,与你们共同学习、共同进步的过程使我受益匪浅。感谢实验室袁磊、刘雨、魏国栋、富强等老师以及机械楼的李敏、周晶晶、石竹、杨绚、毛扬、康仁伟、周博立、张树中和冯康等师弟师妹在博士研究期间给予的帮助。感谢中国科学院软件所周巢尘院士,詹乃军研究员以及软件所一起合作研究的赵恒军、邹亮、权奘等同学在学习形式化方法中给予的极大帮助,感谢中国科学院软件所给予我理论方法以及学习条件上的支持。感谢中国铁道科学研究院的段武研究员给予论文的帮助和指正。感谢我的父母、岳父母以及我的妹妹,是你们一贯的理解和支持才使我得以完成学业。特别感谢我的妻子吴成岩女士,是你的陪伴使我在求学道路上不再寂寞,是你默默地支持与鼓励,才使我顺利完成了四年艰苦的学业。感谢在百忙之中对我的论文进行评阅和指导的各位专家、教授。最后,衷心感谢所有曾经帮助过我的老师、同学和朋友,衷心的祝愿每一个人健康幸福。
和舝中文摘要坪鱯列车运行控制系统虺啤傲锌叵低场是将先进的控制技术、通信技术、计算机技术与铁路信号技术融为一体,保证轨道交通安全、正点、高密度运行的自动化系统。随着计算机在列控系统中的广泛应用,硬件和软件规模不断扩大,系统的复杂性有了很大的提高,呈现出复杂的系统特性⒎⑿浴⑹凳毙院突旌鲜性等等W魑R桓龈丛影踩ǹ燎笙低常锌叵低持腥魏喂收隙加锌赡茉斐芍卮蟮人身伤亡和财产损失,如何保证系统的正确性,寻找一套全面的、有效的建模与验证方法是非常必要的。相比仿真和测试技术,基于严格数学定义的形式化方法不仅能精确、清晰地描述系统结构和相关特性,而且能对特性进行验证,近年来已经成为列控系统建模和验证的一种重要理论方法。论文引入系统层次化建模概念,利用面向对象的建模思想和基于场景的系统设计理念,提出了一套包含系统层、场景层、组件层和功能层的列控系统层次化模型。在此基础上,提出了一个集成西的列控系统分层形式化建模与验证框架。该框架不仅适合列控系统各种特性的验证分析,而且建立的模型具有可继承性、重用性,在保证系统模型一致性的基础上,提高了建模的效率。论文深入分析了列控系统运营场景实时性的验证问题,提出了六种适合于列控系统运营场景描述的时间约束类型:周期性、延迟、时间等待、超时、截止期限和时间中断;提出了的子集模型到时间自动机网络模型的转换规则;给出了运营场景实时性约束的西描述;实现了运营场景中相关实时属性的验证流程。论文深入研究了列控系统运营场景的混合属性验证问题,指出了传统的混杂系统建模与验证方法在刻画列控系统场景中通信行为上存在的不足。并根据现有方法的不足,提出了的假设条件;结合混合自动机的语义,提出了模型到混合自动机模型的转换规则;给出了运营场景中混合属性的西表达;实现了运营场景中相关混合属性的验证流程。【切换场景和行车许可场景魑0咐捶治觥Mü对谢怀【昂托谐敌砜沙【暗姆植阈问交S胙橹し治觯橹ち肆锌叵低的实时性和混合属性,最大限度的避免了系统设计上的缺陷和错误,为进一步解决列控系统建模与验证的关键理论问题,保障列控系统安全可靠的应用和运营提
供重要的理论基础。关键词:列控系统;复杂安全苛求系统;分层建模;验分类号:.北京交通大学博士学位论文