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