原文传递
基于TMSVL的CTCS-3级列控系统建模与验证
| 论文题名： | 基于TMSVL的CTCS-3级列控系统建模与验证 |
| 关键词： | 列车控制系统;时序逻辑;程序设计;TMSVL语言;形式化建模;模型检测 |
| 摘要： | CTCS-3（China Train Control System level3）级列车控制运行系统是保障我国铁路时速300~350 km客运专线高速列车安全、可靠、高效运行的核心技术之一。然而，对于列车控制运行系统这种实时安全关键系统，仅仅依靠经验和自然语言来制定和描述系统的需求规范会难以避免的存在某些缺陷和不安全因素，并且系统的测试若都以现场跑车为主，也会消耗大量的时间和精力。因此，需要一种技术来验证这种实时系统的特性，从而提高系统的正确性或完善系统的功能。基于严格数学定义的形式化方法，由于其能够简洁、准确的描述系统的规格，并验证系统的特性，因此能够作为系统建模和验证的重要理论方法。而时序逻辑作为一种形式化方法，近些年来已经被广泛的运用于实时系统的建模和验证中。 实时建模、仿真及验证语言（Timed Modeling Simulation and Verification Language， TMSVL）是一种基于实时投影时序逻辑（TimedProjection Temporal Logic，TPTL）的实时时序逻辑程序设计语言，它主要用于对实时系统规范的建模、仿真和验证。本文以TMSVL语言作为实时建模、仿真和验证的形式化语言，以我国CTCS-3级列控系统作为建模和验证的对象，提出了一种基于TMSVL语言的CTCS-3级列控系统运营场景形式化建模与验证的方法。文章首先介绍了TPTL和TMSVL的语法和语义，以及其执行平台TMSV（TimedModeling Simulation and Verificationplatform, TMSV），然后简单介绍了CTCS-3级列控系统的结构，并以CTCS-3级列控系统的规范文档作为建模的基础，针对CTCS-3系统规范中的一些核心的运营场景，使用TMSVL语言进行建模，使用实时命题投影时序逻辑（Timed Propositional Projection Temporal Logic， TPPTL）语句描述实时性质和安全性质，最终在其建模和验证环境 TMSV平台中完成了CTCS-3级列控系统的建模、仿真和验证。 |
| 作者： | 苏多铎 |
| 专业： | 计算机科学与技术 |
| 导师： | 王小兵 |
| 授予学位： | 硕士 |
| 授予学位单位： | 西安电子科技大学 |
| 学位年度： | 2015 |
| 正文语种： | 中文 |
检索历史
应用推荐
