列控系统混成行为的建模与验证方法分析

《列控系统混成行为的建模与验证方法分析》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、IIIJIIIIIUlIIIIIIIIIIY2602621学位论文版权使用授权书本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索，提供阅览服务，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国家有关部门或机构送交论文的复印件和磁盘。(保密的学位论文在解密后适用本授权说明)学位论文作者签名：椎锄驾导师签名：．特．．I昭签字日期：矽I峥年印月‘中日签字日期。加f眵年午月／尹日中图分类号：U238学校代码：10004UDC：625密级：公开北京交通大学

2、硕士学位论文列控系统混成行为的建模与验证方法TheModelingandVerificationMethodforHybridBehaviorofTrainControlSystem作者姓名：程瑞军学号：ll120252导师姓名：赵林职称：讲师学位类别：工学硕士学位级别：硕士学科专业：交通信息工程及控制研究方向：列控系统建模与验证北京交通大学2014年3月H致谢首先我要衷心地感谢我的导师赵林老师对我论文的指导。两年多来，老师严谨的治学态度、精益求精的工作态度和平易近人的学者风范，使我受益匪浅：赵老师的悉心指导给我极大的帮助和影响。在此，谨向赵老师致以衷

3、心的感谢和崇高的敬意!感谢实验室的徐田华、郑伟等老师，这些老师在科研工作中为我提出了许多宝贵的意见，您们给予我的帮助，我将终生铭记。此外，我还要感谢我的师兄谢雨飞、刘金涛师兄和李宪、鲁秋子师姐，还有同学何丽芸、程雨、陈耿钦、高僮、齐飞等以及其他师弟师妹们。借此机会，我还要感谢培养我长大含辛茹苦的父母，你们的理解和支持使我能够在学校专心完成学业。谢谢你们!本论文由国家科技部863项目“轨道交通CPS系统的感知、运行和安全技术应用验证”(项目编号：201IAA010104)支持。IV北京交通大学硕士学位论文中文摘要中文摘要摘要：随着列控技术的发展，列车运行

4、控制系统获得了巨大的进步和发展。在系统的设计和开发阶段，为了确保列控系统的安全性，列控系统需求规范的正确性起着越来越重要的作用。然而，在系统开发的初始阶段，通常会因为系统需求规范不完整而无法进行开发。在这种情况下，如何确定系统的关键参数成为主要的研究课题。同时，现有研究成果表明，在需求层面，分析和验证系统模型中的关键参数面临很多困难。因此，为了解决系统模型中关键参数的分析问题，需要提出一种合理的系统属性建模和形式化验证的框架结构。列控系统需求规范的分析过程包括两部的内容，建立系统规范模型和对该形式化模型进行验证。一方面，统一建模语言(LrML)是一种面

5、向对象的建模语言，已广泛应用于不同工程领域。然而，列控系统属于典型的混成系统和安全苛求系统。正确地刻画系统的混成特性给列控系统需求规范的建模工作带来了巨大的挑战。另一方面，形式化方法己成为保障安全苛求系统的安全性与可靠性的重要手段。根据不同的分析或验证要求，设计者可以选择不同的形式化验证工具进行相关的验证工作。因此，本文从列控系统需求规范建模方法与验证工具集成着手进行研究，主要内容包括：1．对列控系统混成特性进行分析，研究UML扩展机制，设计混成UML概要文件，使之能够准确地刻画列控系统的混成特性。2．为了验证混成系统的安全性，提出了时间有界的可达性分

6、析算法。该算法基于BMC验证技术，对具体的自动机模型运用该算法可以计算有界时间内系统的所有可执行路径。时间有界的可达性分析算法适用于线性或非线性混成自动机的验证。3．以移动闭塞中的追踪模型为案例，运用提出的混成UML概要文件对其进行建模；并根据转换规则将所建的列车追踪扩展模型转换为HYTECH模型；在开发的验证支持工具中完成了该模型的验证分析工作。通过案例分析，证明所提出的基于UML扩展机制对列控系统混成行为建模方法的可行性，以及所开发验证支持工具的可用性。4．在Topcased平台上完成了验证工具的软件开发。Topcased平台上集成了UML的建模工

7、具Papyrus，并在Topcased平台上扩展了视re(Views)，将PHAVer和HYTECH等验证工具集成到该平台上，实现对模型的自动化验证，并具备良好的可扩展性。同时提出由扩展后的UML模型到形式化验证模型的转换规则，构造了面向对象语言UML与PHAVer、HYTECH、HySAT等形式化语言之间的转换桥北京交通大学硕士学位论文中文摘要梁。关键词：列控系统：混成特性；信息物理融合系统；UML概要文件；多面体混成自动机验证工具分类号：U238北京交通大学硕士学位论文ABSTRACTABSTRACTABSTRACT：Withthedevelopm

8、entofscienceandtechnology,theTrainControlSystem