基于tmsvl的ctcs-3级列控系统建模与验证

《基于tmsvl的ctcs-3级列控系统建模与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、縣械悼处园胃硕±学位论文＾３圏基于ＴＭＳＶＬ的ＣＴＣＳ－３级列控系统建模与验证作者姓名苏《锋＾邏指导教师姓名、职称王小兵副教授申请学位类别工学硕±ｓ＾西安电子科技大学学位论文独创性（或创新性）声明秉承学校严谨的学风和优良的科学道德，本人声明所呈交的论文是我个人在导师指导下进行的研究王作及取得的研究成果。尽我所知，除了文中特别加Ｗ标注巧致谢中所罗列的内容ｌ＾ｉ，■外论文中不包含其他人已经发表或撰写过的研巧成果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使

2、用过的材料一。与我同工作的同事对本研究所做的任何贡献均己在论文中作了明确的说明并表示了谢意。一学位论文若有不实之处，本人承担切法律责任。Ｌ妙ＳＩ巧］６：斗每键日期本人签名；ｆ西安电子科技大学关于论文使用授权的说明本人完全了解西安电子科技大学有关保留和使用学位论文的规定，目Ｐ；研巧生在校攻读学位期间论文工作的知识产权属于西安电子科技大学。学校有权保留送交论文的复印件，允许查阅、借阅论文；学校可Ｗ公布论文的全部或部分内容，允许采用影印、缩印或其它复制手段保存论文。同时本人保证，结合学位论文研究成果完成的

3、论文、发明专利等成果。，署名单位为西安电子科技大学适。保密的学位论在文＿＿年解密后用本授权书：：本人签名导师签名＇》７｜？日：＞Ｗ；如５７期日期＾３｜叫学校代码10701学号1303121666分类号TP315密级公开西安电子科技大学硕士学位论文基于TMSVL的CTCS-3级列控系统建模与验证作者姓名：苏多铎一级学科：计算机科学与技术二级学科：计算机软件与理论学位类别：工学硕士指导教师姓名、职称：王小兵副教授学院：计算机学院提交日期：2015年11月FormalModelingandVerificationMe

4、thodforCTCS-3SystemUsingTMSVLAthesissubmittedtoXIDIANUNIVERSITYinpartialfulfillmentoftherequirementsforthedegreeofMasterinComputerSoftwareandTheoryBySuDuoduoSupervisor:WangXiaobingAssociateProfessorNovember2015摘要摘要CTCS-3（ChinaTrainControlSystemlevel3）级列车控制运行系统是保障我国铁路时速300~3

5、50km客运专线高速列车安全、可靠、高效运行的核心技术之一。然而，对于列车控制运行系统这种实时安全关键系统，仅仅依靠经验和自然语言来制定和描述系统的需求规范会难以避免的存在某些缺陷和不安全因素，并且系统的测试若都以现场跑车为主，也会消耗大量的时间和精力。因此，需要一种技术来验证这种实时系统的特性，从而提高系统的正确性或完善系统的功能。基于严格数学定义的形式化方法，由于其能够简洁、准确的描述系统的规格，并验证系统的特性，因此能够作为系统建模和验证的重要理论方法。而时序逻辑作为一种形式化方法，近些年来已经被广泛的运用于实时系统的建模和验证中。实时

6、建模、仿真及验证语言（TimedModelingSimulationandVerificationLanguage，TMSVL）是一种基于实时投影时序逻辑（TimedProjectionTemporalLogic，TPTL）的实时时序逻辑程序设计语言，它主要用于对实时系统规范的建模、仿真和验证。本文以TMSVL语言作为实时建模、仿真和验证的形式化语言，以我国CTCS-3级列控系统作为建模和验证的对象，提出了一种基于TMSVL语言的CTCS-3级列控系统运营场景形式化建模与验证的方法。文章首先介绍了TPTL和TMSVL的语法和语义，以及其执行平

7、台TMSV（TimedModelingSimulationandVerificationplatform,TMSV），然后简单介绍了CTCS-3级列控系统的结构，并以CTCS-3级列控系统的规范文档作为建模的基础，针对CTCS-3系统规范中的一些核心的运营场景，使用TMSVL语言进行建模，使用实时命题投影时序逻辑（TimedPropositionalProjectionTemporalLogic，TPPTL）语句描述实时性质和安全性质，最终在其建模和验证环境TMSV平台中完成了CTCS-3级列控系统的建模、仿真和验证。关键词：实时时序逻辑，T

8、MSVL，形式化方法，模型检测，CTCS-3IABSTRACTABSTRACTChineseTrainControlSystemlevel3（CTCS-3）ison