学位论文 > 优秀研究生学位论文题录展示

高速铁路列车运行控制系统的形式化建模与验证方法研究

作　者: 曹源
导　师: 唐涛；穆建成
学　校: 北京交通大学
专　业: 交通信息工程及控制
关键词: 高速铁路列控系统安全苛求系统验证形式化方法定理证明
分类号: U270.3
类　型: 博士论文
年　份: 2011年
下　载: 286次
引　用: 0次
阅　读: 论文下载

内容摘要

高速铁路列车运行控制系统(简称：列控系统)融入了先进的计算机、通信以及控制技术,极大地提升了系统的效率和安全性。由于系统的硬件集成度不断提高,大量软件参与系统控制,使得系统特性也呈现出结构分布、实时性强、响应快速等多样化的趋势,系统特性的验证也愈加困难,因此需要找到一条更为有效、全面的方法实现列控系统的特性验证,进一步提升系统的性能或完善系统功能。基于严格数学定义的形式化方法,由于其能够精确、清晰地描述系统结构和相关特性,同时能够验证系统的相关特性,近年来在列控系统领域得到迅速发展,并且已经成为描述和验证高速铁路列控系统特性的一种重要方法。论文对列控系统的形式化建模、描述以及验证方法的应用展开了综述。分析了RAISE (Rigorous Approach to Industrial Software Engineering,工业软件工程的严格方法)形式化方法在列控系统中建模与验证的优势,并在此基础上,首次将Timed RAISE(时间化RAISE)引入列控系统验证领域。论文研究了基于域+Timed RAISE的高速铁路列控系统的建模和描述方法。结合高速铁路列控系统的实际特点以及复杂性,提出了一种域方法作为系统描述的切入。域方法的主要思想是将系统划分为规模较小的域模型,根据域的验证结果以及域之间的分解与组合关系,能够最终实现大系统的特性验证。论文详细给出了域的元组、域的组合分解以及域特性的组合分解等相关定义和定理,这些定义与定理也是域方法理论体系的关键组成部分。为实现对域方法的更好说明,对典型的高速铁路列控系统—CTCS-3 (China Train Control System level 3)级列控系统进行了实际的域的划分、域模型的建立、域特性的分析、域特性的组合分解以及子域的划分,实现了对域方法理论体系的有力支撑。论文研究了基于域+Timed RAISE的高速铁路列控系统的验证方法。对高速铁路列控系统常见的运营场景描述相关特性、系统功能以及系统性能等三类重要的域特性进行了详细分析,并给出了三类域特性中的场景交互一致性、安全功能以及实时性的定义和数学描述,并作为系统特性验证的重要依据。论文实现了域模型与Timed RAISE结合,给出了域模型转换为TRSL (Timed RAISE Specification Language)的具体规则,同时也给出了在系统TRSL描述的证明过程中相应的推理规则和证明方法。论文对基于域+Timed RAISE的描述和验证方法的具体应用进行了分析和举例。通过对RBC (Radio Block Center,无线闭塞中心)切换场景的交互一致性验证、等级转换(CTCS-2级至CTCS-3级)场景的实时性验证以及两车区间追踪案例中的安全功能进行了实际的域(子域)的划分、系统模型建立、Timed RAISE具体描述以及验证过程。仅为说明基于域+Timed RAISE方法的正确性,将各验证案例都进行了相应的简化和假设。最终给出了结果：列车通过RBC边界的条件下,车载设备与两个RBC的共同交互并不会带来场景交互一致性错误,即场景中各设备和子系统的交互流程是一致的；列车在等级转换(CTCS-2级至CTCS-3级)场景中,即使GSM-R (GSM for Railway)网络的通信随机延迟给场景的实时性带来了巨大的挑战,但依然能够满足场景的实时性要求；在两车追踪案例中,在给定前车以及外界的边界条件后,CTCS-3级列控系统能够在地面设备、车载设备以及GSM-R无线网络的共同作用下实现列车的安全运行。

全文目录

致谢  4-6
摘要  6-8
ABSTRACT  8-14
1 引言  14-24
  1.1 研究背景  14
  1.2 典型高速铁路列控系统特性讨论  14-18
    1.2.1 典型高速铁路列控系统的共性特征  14-16
    1.2.2 高速铁路列控系统相关重要特性  16-17
    1.2.3 典型高速铁路列控系统—CTCS-3级列控系统  17-18
  1.3 高速铁路列控系统的特性验证方法  18-20
  1.4 选题意义  20
  1.5 论文结构与写作安排  20-24
2 形式化方法在列控系统中的应用  24-34
  2.1 概述  24-25
  2.2 基于模型检验的形式化方法  25-27
  2.3 基于定理证明的形式化方法  27-28
  2.4 Timed RAISE方法  28-31
    2.4.1 RAISE背景和由来  28-29
    2.4.2 RAISE描述高速铁路列控系统的优势  29-30
    2.4.3 Timed RAISE的引出  30-31
  2.5 相关形式化方法比较与总结  31-33
  2.6 小结  33-34
3 基于域+Timed RAISE的高速铁路列控系统建模与验证  34-64
  3.1 复杂系统形式化一般性建模与验证框架  34
  3.2 基于域+Timed RAISE高速铁路列控系统建模与验证框架  34-36
  3.3 域以及域组合分解的定义  36-41
    3.3.1 域的定义  37-40
    3.3.2 域的特性元组分解  40-41
  3.4 面向高速铁路的CTCS-3级列控系统的域模型  41-49
    3.4.1 CTCS-3级列控系统运营场景与域模型间关系讨论  42-44
    3.4.2 CTCS-3级列控系统的域模型划分  44-45
    3.4.3 CTCS-3级列控系统的域特性分析  45-46
    3.4.4 CTCS-3级列控系统域的域特性的组合与分解  46-47
    3.4.5 子域的划分  47-49
  3.5 高速铁路列控系统域特性验证分析  49-53
  3.6 域模型的Timed RAISE描述分析  53-59
    3.6.1 域非特性元组的Timed RAISE描述规则  53-56
    3.6.2 域特性元组的Timed RAISE描述规则  56-59
  3.7 Timed RAISE描述具体验证的流程与规则  59-61
  3.8 小结  61-64
4 基于域的场景交互一致性的验证分析  64-78
  4.1 RBC切换场景介绍与假设  64-65
  4.2 RBC切换场景域模型分析  65-67
  4.3 RBC切换域的验证  67-76
    4.3.1 域的相关描述  68-75
    4.3.2 域的场景交互一致性分析以及验证  75-76
  4.4 小结  76-78
5 基于域的实时性的验证分析  78-86
  5.1 等级转换(CTCS-2级至CTCS-3级)基本简介和流程  78-79
  5.2 等级转换(CTCS-2级至CTCS-3级)域的验证  79-85
    5.2.1 域的相关描述  80-84
    5.2.2 域的实时性分析以及验证  84-85
  5.3 小结  85-86
6 基于域的安全功能的验证分析  86-111
  6.1 CTCS-3级列控系统两车追踪控制与系统假设  86-88
    6.1.1 CTCS-3级列控系统的两车追踪场景的基本控制过程  86-87
    6.1.2 两车追踪场景的基本假设  87-88
  6.2 追踪场景的安全需求分析  88-93
    6.2.1 两车追踪的安全需求  89-90
    6.2.2 安全需求基本描述  90-93
    6.2.3 安全运行的描述  93
  6.3 域的描述  93-105
    6.3.1 域的输入  94-100
    6.3.2 子域的划分  100-105
  6.4 域的验证  105-109
    6.4.1 列车的运行  105-107
    6.4.2 两车追踪的初始化  107-109
    6.4.3 safe_move的验证  109
  6.5 小结  109-111
7 结论  111-114
  7.1 论文工作总结  111-112
  7.2 未来工作展望  112-114
参考文献  114-120
附录A RBC切换场景验证过程  120-124
附录B 等级转换场景验证过程  124-126
附录C 两车追踪案例验证过程  126-138
作者简历  138-142
学位论文数据集  142

高速铁路列车运行控制系统的形式化建模与验证方法研究

内容摘要

全文目录

相似论文