基于uml的列控系统建模方法与验证工具集成

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

1、致谢首先我要衷心地感谢我的导师唐涛教授对我论文的指导。两年来，教授严谨的治学态度、精益求精的工作态度和平易近人的学者风范，使我受益匪战：教授的悉心指导给我极大的帮助和影响。在此，谨向唐老师致以衷心的感谢和崇高的敬意!特别感谢实验室的赵林老师。赵老师悉一15,指导我的科研和论文，每当我拿着问题去请教他时，他总是立刻放下手头的工作，认真细致的为我解惑答疑，使我学习了很多知识．提高了自己的能力，在此表示衷心的感谢。感谢实验室的徐田华、郑伟等老师．这些老师在科研工作中为我提出了许多宝贵的意见，您们给予我的帮助，我将终生铭记。此外，我还要感谢我的师

2、兄谢雨飞、刘金涛、i4超、柴铭、刘玉鹏师兄和唐武梅、曹妍师蛆，还有同学李水康、鲁秋子、林虹、周宁以及其他师弟师妹们。借此机会，我还要感谢培养我长大含辛茹苦的父母，你们的理解和支持使我能够在学校专心完成学业。谢谢你们!本论文由国家科技部863项目“轨道交通CPS系统∞感知、运行和安全技术应用验证”(项目编弓：201IAA010104)支持。北京交通大学硕士学位论文中文摘要摘要；近年来随着技术的发展，列车运行控制系统的功能不断增强，为实现不同厂商设备问、地面设备与车载设备问互联互通，使列车能够在轨道交通网中跨线安全运行，列控系统需求规范的作用

3、正日益突显。但现有研究成果表明在需求层面对系统的关键属性进行分析和确认面临很多困难，需要提出一种合理的框架结构以对其关键属性进行建模并对系统进行验证。从速模方法来看．统一建模语言(uML)具有定义良好、易于表达、描述直观等优点，已被广泛应用到不同的领域．但当需要对影响列车安全可靠运行的连续和离散过程进行～体化建模时，对混成特性的描述己远远超出了这种建模语言本身的能力范围，这给列控系统需求规范的建模工作带来了巨大的挑战。从验证方法来看．形式化方法己成为保障安全苛求系统的安全性与可靠性的重要手段。针对不同的系统、同一系统的不同性质和系统分析的

4、不同阶段，可供研究人员使用的形式化验证工具种类繁多。因此，本文从列控系统需求规范建模方法与验证工具集成者手进行研究，主要内容包括：l对列控系统需求规范混成特性建模需求进行分析，研究UML扩展机制，充分挖掘UML的图形功能，设计面向列控系统需求规范的混成UML概要文件，使之能够包含更多的内容与信息去准确地刻画列控系统的混成特性。2在论述列控系统需求规范的分析方法体系结构的基础上，重点分析了模型验证阶段的功能需求。在Eclipse平台上完成了验证支持工具的软件原型开发，对底层形式化建模过程和验证工具进行封装，通过自动化的模型检验技术来寻找需求

5、中脖藏的错误，使现有的需求管理工具(IBMRequisitePro)、建摸工具fIBMRationalSottwareArchited、和验证1具(NuSMV，PHAVer)实现高度集成，并具备良好的可扩展性。并给出MUML模型到形式化模型的转换规则．构造了面向对象语言UML以及NuSMV、PHAVer形式化语言之间的转换桥梁。3从列控系统需求规范中选取了具有代表性的模式转换场景和RBC交接场景，利用所提出的混成UML概要文件对场景进行建模；将建好的模式转换场景模型转换为NuSMV模型，而将RBC交接场景模型转换为PHAVcr模型；在开发

6、的验证支持工具中完成两个形式化模型的验证分析工作。通过案例分析，证明文中所提出的基于UML扩展机制的列控系统需求规范建模方法的可行性．以及所开技验证支持工具的可用性。关键词：列控秉统；需求规范：UML概要文件；验证支持工具：PHAVer；NuSMV分类号．u2：：垫室奎塑查堂翌主兰堡堕兰!奎些墨北京交通大学硕士学位论文ABSTRACTABSTRACT：Withthedevelopmentofscienceandtechnology，TrainControlSystem’functionshavedevelopedintoanewstage

7、Inordertorealizetheconnectionbetweendifferentequipmentsproducedbydifferentmanufactures，andtoinsurethesafetyoftheTrainControlSystematthesametime，TrainControlSystem’sSystemRequirementSpecification(SRS)hasplayedamoreandmoreimpertsntroleinresearchanddevelopmentHowever，current

8、studiesshowthatthereexistalotofdifficultiesfortheanalysisandvalidationworkofthecriticalpropertie