探索ctcs-3级列控系统的uml建模与模型检验研究

《探索ctcs-3级列控系统的uml建模与模型检验研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、北京交通大学硕士学位论文CTCS-3级列控系统的UML建模与模型检验研究姓名：吴晓丹申请学位级别：硕士专业：交通信息工程及控制指导教师：宁滨201012中文摘要摘要：CTCS．3级列车运行控制系统是基于GSM．R无线传输系统实现安全控制信息双向传输的列车运行控制系统，是中国列车控制系统的重要组成部分。为了实现客运专线列车运行控制系统的国产化，必须研究适用于客运专线的CTCS3级技术规范和关键技术，形成中国高速客运专线列车运行控制系统的技术体系。在系统开发中，建立模型是研究系统的重要手段和前提。建立的

2、模型首先必须易于开发人员理解和使用，其次模型必须正确地反映系统的需求，最后列车运行控制系统模型的安全性也是一个需要关注的问题。UML是一种通用可视化建模语言，易于理解和掌握因而适合于团队开发。然而UML本身没有提供验证模型正确性的手段，因此需要采用其他方法对UML模型进行检验。符号模型检验技术是形式化验证中很重要的一种方法，适用范围广、速度快且充分自动化。本文利用符号模型检验系统对UML模型进行检验。在模型检验的基础上本文得出了系统的SMV模型，之后利用故障注入技术对得到的SMV模型进行了相关的安全

3、性分析。首先，本文对CTCS．3级列控系统级间转换场景进行了分析，然后对其进行UML建模得到UML类图和UML状态图。UML类图给类增加了表示系统组成之间信息交互的输入输出事件，UML状态图主要表示对象在输入事件的触发下发生状态转移并产生输出事件。在对建立好的UML模型进行检验之前，需要把UML模型转换为SMV模型。UML类图中的每个类在SMV模型中对应的是它的一个SMv模块，而类所对应的对象的状态转移则由相应的SMV模块中状态变量的更新来表达。本文在转换中建立了转换的一般规则。符号模型检验中，系统

4、性质是用计算树逻辑公式CTL表达的。把系统的SMv模型和系统性质输入符号模型检验系统就可以检验系统性质如可达性、活性等。检验结果为Tme，则说明系统满足给出的性质；检验结果为False，则说明SMv模型或UML模型存在错误，可以根据反例进行相应的分析。在对系统的SMV模型修改使其满足所有给出的性质后，可以利用故障注入技术把故障注入到SMV模型中。系统的安全性质同样可以通过CTL公式来表达，之后就可以检验系统的安全性质。故障树的结构函数是一个布尔函数，利用sMv可以得到布尔函数的真值表并生成一个故障树

5、。关键词：CTCS．3；UML；符号模型检验；SMV；故障注入分类号：U284ABSTRACTABSTRACT：CTCS-3TrainControlSyst锄lsasystemwhichisbasedonGSM-Rwarelesst啪smissionsystemfordeliVeringbidirectionalsa屁controlinfo册ation，觚disaveryimport觚tcomponentpanofChinaTrainCon仃olSystem(CTCS)．111orderformel

6、ocalizationofthepassellgerdedicatedlineTrainControlSystelll，ItisnecessarytoinVestigatet11etechnicalsp鲥矗cationandkeytecllllolog)rofCTCS一3TrainControlSystemofpaSseIlgerdedicatedline，fomlingthetecllIlicalsyst锄ofCllinahi曲speedp嬲sengerd甜icatedlineThinColl仃0

7、lSyst锄．ModelingisaVe拶iII：Il，ortantmethodandpre嘲uisiteiIlsystemdesi印．First，modelmustbeeasyfordesignerto吼derstaIldanduse．Secondly；modelneedt0renectⅡlesyst锄requi崩nentscom沁tly．Saf-etyoftllemodelofTrainControlSystemisalsoais跚eneedtopayattentiont0．UMLisaumVe

8、rsalVisualmodelinglauguage，nisSuitedforteamworkdesi弘雒itiseasyt0uIlderst锄dandmaSt既HoweV％UMLdoeSn’tof】衙ametllodt0checknleco玎．cc恤essofmemodelitself：Tl】啪，UMLmodelneedtobecheckedbyotllermealls．S)，InbolicModelCheckingisaVe巧si班ficantmetllodof缸