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

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

作　者: 秦玲
导　师: 穆建成
学　校: 北京交通大学
专　业: 交通信息工程及控制
关键词: 中国列车运行控制系统应用等级3 无线闭塞中心 Statemate 形式化建模数据库设计数据流生成
分类号: U284.48
类　型: 硕士论文
年　份: 2009年
下　载: 100次
引　用: 1次
阅　读: 论文下载

内容摘要

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

全文目录

致谢  5-6
中文摘要  6-7
ABSTRACT  7-11
1 综述  11-17
  1.1 研究背景简介  11-13
    1.1.1 CTCS-3列控系统原理及组成  11-12
    1.1.2 无线闭塞中心数据流的重要性  12-13
  1.2 国内外数据库研究现状  13-15
    1.2.1 数据库技术  13-14
    1.2.2 数据库开发方法  14-15
  1.3 选题的目的及意义  15-16
  1.4 论文的研究内容和结构安排  16-17
2 Statemate及其理论基础  17-23
  2.1 形式化方法简介  17
  2.2 实时嵌入式开发环境Statemate  17-21
    2.2.1 Statemate的特点  18-19
    2.2.2 Statemate的建模语言  19-20
    2.2.3 选择Statemate的原因  20-21
  2.3 有限状态机  21-22
    2.3.1 有限状态机的相关概念  21-22
    2.3.2 有限状态机的分类及应用  22
  2.4 本章小结  22-23
3 无线闭塞中心数据库设计与数据生成  23-42
  3.1 无线闭塞中心数据库需求分析  23-28
    3.1.1 列车的注册与启动  23-25
    3.1.2 RBC切换  25-26
    3.1.3 计算行车许可  26-28
  3.2 无线闭塞中心数据库的组成及结构划分  28-33
    3.2.1 按照功能划分  28-31
    3.2.2 线路静态数据库  31-32
    3.2.3 各部分关系  32-33
  3.3 线路静态数据库  33-36
    3.3.1 线路静态数据存储和生成  33
    3.3.2 线路静态数据库结构  33-36
  3.4 数据流模型  36-41
    3.4.1 RBC配置数据流模型  37-38
    3.4.2 进路区段信息数据流模型  38
    3.4.3 区间区段信息数据流模型  38-40
    3.4.4 列车初始位置有效性数据流模型  40
    3.4.5 LRBG位置有效性数据流模型  40-41
  3.5 本章小结  41-42
4 无线闭塞中心数据流仿真验证分析  42-69
  4.1 运营场景下无线闭塞中心数据流模型  42-61
    4.1.1 注册与启动  42-51
    4.1.2 RBC切换  51-55
    4.1.3 计算行车许可  55-61
  4.2 数据库模型功能和行为仿真与验证  61-68
    4.2.1 模拟仿真  61-63
    4.2.2 形式化验证  63-68
  4.3 本章小结  68-69
5 总结与展望  69-71
  5.1 总结  69-70
  5.2 展望  70-71
参考文献  71-73
图索引  73-74
表索引  74-75
作者简历  75-77
学位论文数据集  77

相似论文

微型农业气象信息系统分析与设计,TP311.52
浙江纺织服装职业技术学院网络考试系统的设计与实现,TP311.52
水库群防洪调度决策支持系统设计与开发研究,TP311.52
四川职业技术学院体育场馆管理信息系统的设计与实现,TP311.52
E-commerce Online Book Store and It\'s Security Research,F713.36
电视广告商务平台中Oracle数据库的ADICI设计与优化研究,TP311.13
动态分段技术在UTGIS中的应用研究,P208
基于形式化建模的安全缺陷知识库的构建,TP393.09
基于J2EE的出版类企业电子商务系统平台研究与设计,TP311.52
教育科研信息资源管理系统的设计与实现,TP311.52
科研项目计划及过程管理系统的设计与实现,TP311.52
基于EJB技术的网络考试系统开发研究,TP311.52
衡水工业学校药房管理系统的设计与实现,TP311.52
职业学校学生成绩管理系统的设计实现,TP311.52
南昌邮区中心局生产管理系统的设计和实现,TP311.52
航空活塞发动机试车台设计及测试系统开发,V263.4
政府电子信访系统构建研究,D632.8
油田生产分析及管理系统开发研究,TP311.52
网上教学系统的设计和实现研究,TP311.52
基于WEB的山东工业职业学院评教系统的设计与实现,TP311.52
炮兵战场情报处理系统软件设计及实现,TP311.52