基于STATEMATE的无线闭塞中心数据流生成及形式化验证

摘要

CTCS-3级列控系统是基于无线通信的列车运行控制系统，是中国列车运行控制系统（CTCS）的重要组成部分，代表现有的中国列车运行控制技术的先进水平。无线闭塞中心（RBC）是CTCS-3级列控系统的地面子系统的关键设备。 无线闭塞中心数据库是无线闭塞中心的重要组成部分，它负责管理无线闭塞中心在整个控车过程中从外部设备接收到的数据。生成无线闭塞中心数据流的目的是将存储在无线闭塞中心数据库中的数据分类整理成无线闭塞中心应用层（RBC中其他应用模块）所需的形式，为无线闭塞中心计算行车许可（MA）提供必要数据支持。由此可见，无线闭塞中心数据流的生成对于保证列车在RBC管辖范围内线路上的安全运行起到至关重要的作用，因此对无线闭塞中心数据流生成的研究有很大的实际意义。 论文首先以CTCS-3级列控系统主要运营场景中无线闭塞中心应实现的功能为根据，对每个运营场景下无线闭塞中心数据库的功能需求进行具体分析。从功能需求入手设计无线闭塞中心数据库，并对数据库设计进行规范化，使其能在保证功能需求的前提下，提高性能。 鉴于形式化方法可以减少设计错误、提高系统可信性的特点，论文选择了形式化建模作为研究方法，并以面向功能需求的复杂实时嵌入式系统自动设计软件包Statemate为平台，设计无线闭塞中心数据流，并对设计进行建模分析，以确保设计与需求匹配。 论文利用Statemate核心建模语言之一——离散状态图，分别建立注册与启动、RBC切换、计算行车许可三个场景下无线闭塞中心数据流生成的状态转移模型，描述RBC应用层调用无线闭塞中心数据流模型实现控车功能的过程，并利用Statemate自带的模拟仿真器和模型检验模块，对数据流模型进行形式化的验证和分析，有效地排除了系统设计中存在的矛盾、二义性、含糊性等情况，保证无线闭塞中心数据流模型的设计切实满足功能需求和安全性需求，为设计无线闭塞中心数据流的生成提供了理论依据。

目录

文摘

英文文摘

论文说明：图表目录

声明

致谢

1 综述

1.1 研究背景简介

1.1.1 CTCS—3列控系统原理及组成

1.1.2 无线闭塞中心数据流的重要性

1.2 国内外数据库研究现状

1.2.1 数据库技术

1.2.2 数据库开发方法

1.3 选题的目的及意义

1.4 论文的研究内容和结构安排

2 Statemate及其理论基础

2.1 形式化方法简介

2.2 实时嵌入式开发环境Statemate

2.2.1 Statemate的特点

2.2.2 Statemate的建模语言

2.2.3 选择Statemate的原因

2.3 有限状态机

2.3.1 有限状态机的相关概念

2.3.2 有限状态机的分类及应用

2.4 本章小结

3 无线闭塞中心数据库设计与数据生成

3.1 无线闭塞中心数据库需求分析

3.1.1 列车的注册与启动

3.1.2 RBC切换

3.1.3 计算行车许可

3.2 无线闭塞中心数据库的组成及结构划分

3.2.1 按照功能划分

3.2.2 线路静态数据库

3.2.3 各部分关系

3.3 线路静态数据库

3.3.1 线路静态数据存储和生成

3.3.2 线路静态数据库结构

3.4 数据流模型

3.4.1 RBC配置数据流模型

3.4.2 进路区段信息数据流模型

3.4.3 区间区段信息数据流模型

3.4.4 列车初始位置有效性数据流模型

3.4.5 LRBG位置有效性数据流模型

3.5 本章小结

4 无线闭塞中心数据流仿真验证分析

4.1 运营场景下无线闭塞中心数据流模型

4.1.1 注册与启动

4.1.2 RBC切换

4.1.3 计算行车许可

4.2 数据库模型功能和行为仿真与验证

4.2.1 模拟仿真

4.2.2 形式化验证

4.3 本章小结

5 总结与展望

5.1 总结

5.2 展望

参考文献

作者简历