（交通信息工程及控制专业论文）基于STATEMATE的无线闭塞中心数据流生成及形式化验证.pdf

中文摘要 摘要：c t c s 3 级列控系统是基于无线通信的列车运行控制系统，是中国列车运行 控制系统( c t c s ) 的重要组成部分，代表现有的中国列车运行控制技术的先进水平。 无线闭塞中心( r b c ) 是c t c s 3 级列控系统的地面子系统的关键设备。 无线闭塞中心数据库是无线闭塞中心的重要组成部分，它负责管理无线闭塞 中心在整个控车过程中从外部设备接收到的数据。生成无线闭塞中心数据流的目 的是将存储在无线闭塞中心数据库中的数据分类整理成无线闭塞中心应用层 ( 1 m c 中其他应用模块) 所需的形式，为无线闭塞中心计算行车许可( m a ) 提供 必要数据支持。由此可见，无线闭塞中心数据流的生成对于保证列车在r b c 管辖 范围内线路上的安全运行起到至关重要的作用，因此对无线闭塞中心数据流生成 的研究有很大的实际意义。 论文首先以c t c s 3 级列控系统主要运营场景中无线闭塞中心应实现的功能 为根据，对每个运营场景下无线闭塞中心数据库的功能需求进行具体分析。从功 能需求入手设计无线闭塞中心数据库，并对数据库设计进行规范化，使其能在保 证功能需求的前提下，提高性能。 鉴于形式化方法可以减少设计错误、提高系统可信性的特点，论文选择了形 式化建模作为研究方法，并以面向功能需求的复杂实时嵌入式系统自动设计软件 包s t a t c m a t e 为平台，设计无线闭塞中心数据流，并对设计进行建模分析，以确保 设计与需求匹配。 论文利用s t a t c m a t e 核心建模语言之一离散状态图，分别建立注册与启动、 r b c 切换、计算行车许可三个场景下无线闭塞中心数据流生成的状态转移模型， 描述r b c 应用层调用无线闭塞中心数据流模型实现控车功能的过程，并利用 s t a t e m a t e 自带的模拟仿真器和模型检验模块，对数据流模型进行形式化的验证和 分析，有效地排除了系统设计中存在的矛盾、二义性、含糊性等情况，保证无线 闭塞中心数据流模型的设计切实满足功能需求和安全性需求，为设计无线闭塞中 心数据流的生成提供了理论依据。 本论文共有图3 4 幅，表1 4 个，参考文献5 0 篇。 关键词：中国列车运行控制系统应用等级3 ；无线闭塞中心；s t a t c m a t e ；形式化建 模；数据库设计；数据流生成 分类号：1 1 2 8 a b s t r a c t a b s t r a c t ： c h i n at r a i n c o n 臼o l s y s t e m l e v e l 3 ( c t c s - 3 ) i sa c o m m u n i c a t i o n - b a s e dt r a i nc o n t r o ls y s t e m i ti sa ni m p o r t a n tc o m p o n e n to fc h i n a t r a i nc o n t r o ls y s t e m ( c t c s ) i ti so nb e h a l fo ft h ea d v a n c e dl e v e li nt h ee x i s t i n gt r a i n c o n t r o lt e c h n o l o g y r a d i ob l o c kc e n t e r ( r b c ) i st h ek e ye q u i p m e n to ft h et r a c k s i d e s u b - s y s t e mi nc t c s 一3 r b cd a t a b a s ei sa l li m p o r t a n tp a r to fr b c i ti sr e s p o n s i b l ef o rt h em a n a g e m e n to f d a t a , w h i c hi s r e c e i v e df r o me x t e r n a le q u i p m e n t si nt h ew h o l ep r o c e s so ft r a i n c o n t r 0 1 t h ep u r p o s eo fg e n e r a t i n gr b cd a t as t r e a m si ss o r t i n go u tt h ed a t as t o r e di n r b cd a t a b a s ei n t ow h a t e v e rf o r m a tr b ca p p l i c a t i o nl a y e r ( t h eo t h e ra p p l i c a t i o n m o d u l e so fl m c ) n e e d s ，p r o v i d et h en e c e s s a r yd a t as u p p o r tf o rr b ct oc o m p u t e m o v e m e n ta u t h o r i t y ( m a ) b yt h i st o k e n , t h eg e n e r a t i o no fr b cd a t as t r e a m sp l a y sa v e r yc r u c i a lr o l ei ne n s u r i n gt h a tt h et r a i n sw h i c ha r ew i t h i nt h ej u r i s d i c t i o no ft h er b c c a nio ns a f e l y t h e r e f o r e , t h es t u d yo ft h eg e n e r a t i o no fr b cd a t as t r e a m sh a sg r e a t p r a c t i c a ls i g n i f i c a n c e f i r s t l y , a c c o r d i n gt ot h es p e c i f i e df u n c t i o nw h i c hr b cs h o u l dr e a l i z ei nt h em a i n r m l w a yo p e r a t i o ns c 髓懿o fc t c s 一3 ，t h et h e s i sm a k e sac o n c r e t ea n a l y s i so ff u n c t i o n a l r e q u i r e m e n to fr b cd a t a b a s ei ne v e r yo p e r a t i o ns c e n e 1 1 1 i sp a p e rb e 萄璐t od e s i g n r b cd a t a b a s ew i mt h ef u n c t i o n a lr e q u i r e m e n to fr b cd a t a b a s e , a n dn o r m a l i z e st h e d e s i g nt oi m p r o v et h ep e r f o r m a n c eo fr b cd a t a b a s e , o nt h ep r e m i s eo fa c h i e v i n g f u n c t i o n a l t h ef o r m a lm e t h o d sh a v et h ea d v a n t a g eo fr e d u c i n gd e s i g ne l l o r sa n di m p r o v i n g s y s t e mr e l i a b i l i t y i nv i e wo ft h e s ec h a r a c t e r i s t i c s ，t h i sp a p e rc h o s e sm o d e l i n gb a s e do n f o r m a lm e t h o d sa sr e s e a r c hm e t h o d s t a t e m a t ee n a b l e se n g i n e e r st or a p i d l yd e s i g na n d v a l i d a t ec o m p l e xr e a c t i v es y s t e m st h r o u g hau n i q u ec o m b i n a t i o no fg r a p h i cm o d e l i n g , s i m u l a t i o n , c o d eg e n e r a t i o n , d o c u m e n t a t i o ng e n e r a t i o n ，a n dt e s tp l a nd e f i n i t i o n a sa r e s u l t ，t h et h e s i sc h o s e ss t a t e m a t ea sr e s e a r c hp l a t f o r mt od e s i g nt h ea p p l i c a t i o n so f r b cd a t a b a s ea n dm o d e l st h ed e s i g nf o re n s u r i n gt h a tt h ed e s i g no fr b cd a t as t r e a m s m a t c hw i t ht h ef u n c t i o n a lr e q u i r e m e n t s t a t ec h a r ti so n eo ft h ec o r em o d e l i n gl a n g u a g e si ns t a t e m a t e s ot h i sp a p e re a c h e s t a b l i s h e ss t a t et r a n s i t i o nm o d e l so ft h ea p p l i c a t i o n so fr b cd a t as t r e a m sw i t hs t a t e c h a r t ，i nt h r e er a i l w a yo p e r a t i o ns c e n e sw h i c ha r e l o g i na n ds t a r t i n g ，r b ch a n d i n g o v e r a n d “c o m p u t i n gm a t h e s em o d e l ss h o wt h ep r o c e s st h a tr b ca p p l i c a t i o nl a y e r c a l l sr b cd a t as t r e a m st or e a l i z et h ef u n c t i o n a lo ft r a i nc o n t r 0 1 t h ep a p e ru s e st h e s i m u l a t i o nt o o la n dc h e c km o d e lt o o lw i t h i ns t a t e m a t et om a k ea c c u r a t es i m u l a t i o na n d r i g o r o u sv a l i d a t i o nf o rt h e s em o d e l so fr b cd a t as t r e a m s i nt h i sw a y , t h et h e s i s e f f e c t i v e l ye l i m i n a t e st h ee x i s t i n gc o n t r a d i c t i o n sa n dt h ea m b i g u i t y i nt h es y s t e m o r i g i n a ld e s i g n , t , 1 l s u r e s t h a tt h e d e s i g no fr b cd a t a b a s em e e t s f u n c a t i o n a l r e q u i r e m e n t sa n ds e c u r i t yr e q u i r e m e n ta l s o t h e s ec o n c l u s i o n sp r o v i dt h et h e o r e t i c a l b a s i sf o rt h ed e s i g no fr b cd a t as t r e a m s k e y w o r d s ：c t c s - 3 ；r b c ；s t a t e m a t e ；f o r m a lm o d e l i n g ；d a t a b a s ed e s i g n , g e n e r a t i o no fd a t as t r e a m s c l a s s n o ：u 2 8 v 图索引 图l lr b c 应用软件总体结构图 图2 一ls t a t e m a t e 软件结构图 图2 - 2s t a t e m a t e 的建模语言与视图的关系 图3 - l 砒妃切换运营场景1 5 图3 - 2r b c 应用整体数据流 图3 _ 3 无线闭塞中心数据库组成 图3 _ 4 无线闭塞中心数据库各部分关系2 2 图3 - 5 数据之间结构关系2 5 图3 - 6 线路静态数据库类图 2 6 图3 - 7 线路静态数据使用流程2 7 图3 _ 8r b c 配置数据流模型2 7 图3 _ 9 进路区段信息数据流模型2 8 图3 - l o 区间区段信息数据流模型2 9 图 l l 列车初始位置有效性信息流模型。 3 0 图 1 2u m g 位置有效性信息流模型3l 图o l 注册与启动顺序图模型。3 3 图4 _ 2 注册与启动数据流生成离散状态总模型图3 5 图4 弓注册与启动之初始化数据流生成离散状态子模型图3 6 图4 - 4 注册与启动之建立通信数据流生成离散状态子模型图3 7 图4 5 注册与启动之消息管理数据流生成离散状态子模型图3 9 图4 - 6r b c 切换数据流生成功能结构模型图。4 l 图4 _ 7r b c 切换之移交数据流生成离散状态模型图4 2 图4 - 8r b c 切换之接收数据流生成离散状态模型图4 4 图4 巧m a 计算数据流生成总离散状态模型图4 5 图4 - 1 0m a 计算之计算列车行驶路径数据流生成离散状态模型图。4 6 图知l l 计算列车行驶路径一从车站开始添加区段离散状态模型图。4 8 图4 - 1 2 计算列车行驶路径从区间添加区段离散状态模型图5 0 图4 _ 1 3s t a t e m a t e 仿真环境5 l 图4 - 1 4 注册与启动离散状态模型仿真过程。5 2 图4 - 1 5 注册与启动离散状态模型仿真结果5 3 图4 - 1 6s t a t e m a t e 验证环境5 4 图4 _ 1 7 注册与启动离散状态模型初步验证结果5 4 图4 _ 1 8 注册与启动离散状态模型最终验证结果5 5 图4 - 1 9 验证结果5 6 表索引 表4 - l 注册与启动顺序图模型组成解析 表4 - 2 注册与启动时序模型图变量名解析3 4 表4 _ 3 注册与启动数据流生成离散状态总模型图变量注释3 5 表4 _ 4 注册与启动之初始化数据流生成离散状态子模型图变量注释表3 6 表4 _ 5 注册与启动之建立通信数据流生成离散状态子模型图变量命名解释3 8 表4 _ 6 注册与启动之消息管理数据流生成离散状态子模型图变量命名解释3 9 表4 0r b c 切换数据流生成功能结构模型图变量注释。4 1 表4 墙r b c 切换之移交数据流生成离散状态模型图变量注释4 2 表4 _ 9r b c 切换之接收数据流生成离散状态模型图变量注释。4 4 表4 - 1 0m a 计算数据流生成总离散状态模型图变量注释。4 5 表4 - llm a 计算之计算列车行驶路径数据流生成离散状态模型l 鲴变量注释4 6 表4 - 1 2 计算列车行驶路径一从车站开始添加区段离散状态模型图变量注释4 9 表4 _ 1 3 注册与启动场景下无线闭塞中心数据需求与设计对比5 6 表4 _ 1 4 行车许可计算和发送场景下无线闭塞中心数据需求与设计对比5 7 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作 了明确的说明并表示了谢意。 学雠文储躲翩签字吼叫年月缈日 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国 家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学能文储躲孙 导师躲 签字日期：年r 月9 日 致谢 本论文的工作是在我的导师穆建成教授的悉心指导下完成的。两年以来，穆 建成教授严谨的治学态度和科学的工作方法给了我极大的帮助，同时穆建成教授 开放的思维和细心负责的态度也一直影响着我。在此衷心感谢穆老师在我研究生 期间对我学业上关心和指导，以及生活上的教诲和启迪，这些都将是我在日后工 作生活中巨大的财富，我将始终铭记在心。 唐涛教授、王海峰教授、马连川教授都对我的科研工作和论文都提出了许多 的宝贵意见，在此对他们表示衷心的感谢。刘中田、袁磊老师悉心指导我完成了 实验室的科研工作，在学习上和实验室的科研工作中都给予了我很大的关心和帮 助，在此向刘中田老师、袁磊老师致以十二万分的谢意。 在实验室工作及撰写论文期间，刘超、陈磊、吕继东等博士师兄在我研究生 学习期间都给了我很多的帮助和指导，在此对他们的热心帮助表示感谢。同时还 要感谢实验室的李伟、梁楠、耿鹏、杨韬、王艳等同学，感谢他们对我论文的研 究工作给予的热情帮助。 感谢一直和我站在一起并肩作战的杨扬、刘丽娟、王观宁、孙伟等同学，他 们认真的态度和坚持的信念都是我学习内容，同时他们的支持和鼓励也给我了奋 斗的动力和信心，在此向他们表达我的感激之情。 另外我要感谢我的父母，感谢他们付出辛酸和汗水把我养育成人。也因为有 他们的理解和支持，我才能在学校专心完成我的学业，才能坚强面对学习生活中 的困难和挫折，才能勇敢的追求我的理想。 本论文由国家自然科学基金项目“列车运行控制及组织的基础理论与关键技 术研究一( 项目号：6 0 6 3 4 0 1 0 ) 支持。 1 综述 搿十一五一以来，中国铁路进入了新的发展时期，铁路技术创新实现历史性 跨越。为确保列车运行安全和提高运输效率，迫切需要装备性能先进、安全可靠 的列车运行控制系统f l 】。因此对于先进列车运行控制系统c t c s 3 级列控系统 的研究，将会为中国铁路进一步发展奠定坚实的理论基础，同时也为中国铁路进 一步发展提供强而有力智力支持。 1 1 研究背景简介 1 1 1c t c s 3 列控系统原理及组成 c t c s - 3 级列车运行控制系统是中国列车运行控制系统( c t c s ) 的重要组成 部分之一，它采用无线通信系统( 如g s m r ) 实现地面一列车之间连续、双向的 信息传输，即c t c s 3 级是基于无线通信的列车运行控制系统【2 l 。 c t c s - 3 级地面子系统 c t c s 3 级地面设备的组成包括：无线闭塞中心( 1 国c ) ；调度集中系统( c t c ) ： 联锁系统( i c ) ；列控中心( t c c 3 】) ；轨道电路：应答器( b a l i s e ) ；g s m r 网络。 c t c s - 3 级地面设备的主要功能包括【4 】：在地面设备区域内，通过列车的c t c s 标识号获得列车的信息；通过轨道电路获取轨道占用信息以便跟踪区域内的列车； 根据调度命令、进路信息和轨道占用等信息，生成管辖范围内每一列列车的行车 许可；接收调度集中系统( c t c ) 提供的临时限速信息；通过g s m r 向管辖范围 内的列车传送列车当前的行车许可、临时限速及线路参数等信息；地面应答器负 责提供列车定位基准信息及列车运行方向信息；根据需要产生紧急停车信息、文 本显示信息等，并通过g s m r 传送给相应的列控车载设备。 c t c s 3 级车载子系统 c t c s - 3 级车载设备的组成包括：车载安全计算机；人机接口( d m i e 3 】) ；记录 器：应答器传输模块( b t m ) ；专用传输模块( s t m ) ；g s m r 移动台( m t ) 。 c t c s - 3 级车载设备的主要功能包括【4 】：通过g s m r 接收地面传输的行车许 可、临时限速及线路参数等信息，同时向地面设备传送列车的动态信息( 如列车 速度、位置等) ；接收地面应答器提供的定位基准信息、列车运行方向信息、等级 转换等；实时测量列车的运行速度和走行距离等；实时计算目标距离模式控制曲 线，监督列车安全运行；列车速度超过允许速度时，根据超速情况自动实施常用 制动或者紧急制动：显示列车的运行速度、允许速度、目标速度和目标距离等； 以语音或声光报警方式显示工作状态；记录c 3 系统设备状态、司机操作等信息。 1 1 2无线闭塞中心数据流的重要性 无线闭塞中心( 1 m c ) 是c t c s - 3 级列控系统的地面子系统的关键设备。无线 闭塞中心( r b c ) 是一个基于计算机的系统【5 】，根据从外部轨旁系统得到的基本信息 ( 股道占用信息和进路信息等) 以及从车载子系统得到的信息( 如位置报告) 产 生传输给车载子系统的信息。这些信息的主要目的这些消息的主要目的是向车载 设备提供行车许可( m a ) 、相应的线路参数、临时限速等信息，使列车在r b c 管 辖范围内的线路上安全运行。 图i ir b c 应用软件总体结构图 f i g u r e1 - 1o v e r a l ls 仃u c t u r eo f r b ca p p l i c a t i o ns o f t w a r e 无线闭塞中心主要功能包括：系统自检、无线通信管理、行车许可管理、列 2 车信息管理、r b c 交接管理、消息处理、静态数据管理等，而这些功能的实现都 离不开数据的支持。 r b c 系统自检时与c t c 、联锁、列控中心、无线设备、相邻r b c 等设备 建立通信联系，需要通信配置信息； 在无线通信管理过程中需要管理无线通信中的消息； 行车许可生成及管理需要线路信息、临时限速信息； 列车信息管理需要实时更新包括列车速度、工作模式、c t c s 等级等列车 动态数据； r b c 交接管理过程中需要相邻r b c 的电话号码与交接应答器的信息： r b c 功能的实现需要依靠内部多个模块的相互配合，同时还需要与其他子系 统协同工作，因而其规模庞大，控制机理相当复杂，属于对实时性、可靠性要求 高的一种控制系统。生成无线闭塞中心数据流的目的是将存储在无线闭塞中心数 据库中的数据分类整理成无线闭塞中心应用层( 1 m c 中其他应用模块) 所需的形 式，为无线闭塞中心计算行车许可( m a ) 提供必要数据支持，所以与r b c 内部 的每个模块之间都存在数据交互。由此可知，设计生成的无线闭塞中心数据流是 否满足功能需求直接关系到无线闭塞中心的功能能否实现，关系到列车在r b c 管 辖范围内能否安全行驶。因此，本文对无线闭塞中心数据流生成的研究是相当有 意义的。 1 2国内外数据库研究现状 1 2 1数据库技术 目前数据库技术主要类型有：关系数据库系统【6 】、分布式数据库系统f 7 1 、并行 数据库系统i 舯、面向对象数据库系统、时态数据库系统【9 】、嵌入式数据库系统【1 0 1 、 空间数据库系统【l l 】、工程数据库f 1 2 】等。 几种主要数据库系统在数据库中所占地位 关系数据库系统【6 】 所谓关系型数据库，是指采用了关系模型来组织数据的数据库。目前，关系 数据库系统在应用上占主导地位。 分布式数据库系统【7 1 分布式数据库系统是物理上分散逻辑上集中的数据库系统。随着微机和计算 机局域网、高速信息网的飞速发展，分布式数据库系统在信息技术领域中的重要 性日渐显著。 面向对象数据库系统网 因需要数据库具备结构模拟与行为模拟的特征性，面向对象数据库已成为数 据库发展的重要方向之一。它将数据与操作方式统一为整体的一个对象，将数据 及其过程一起封装起来。由于面向对象数据库在数据库中引人面向对象的数据模 型和方法，在建模化能力和运行性能上均显示出比关系数据库具有更大的优越性 和潜力，它能够很好地支持多种非常规数据库应用。 实时数据库系统【1 3 】 实时数据库( r t d b - - r e a l i t m ed a t a b a s e ) 是数据库系统发展的一个分支，是 数据库技术结合实时处理技术产生的。实时数据库系统是开发实时控制系统、数 据采集系统、c i m s 系统等的支撑软件。在流程行业中，大量使用实时数据库系统 进行控制系统监控，系统先进控制和优化控制，并提供生产管理和调度、数据分 析、决策支持及远程在线浏览实时数据服务和多种数据管理功能。 嵌入式数据库系统【i o l 嵌入式数据库系统是指支持移动计算或某种特定计算模式的数据库管理系 统，它通常与操作系统和具体的应用集成在一起，运行在嵌入式或者移动设备上。 嵌入式数据库技术涉及嵌入式、数据库以及移动通讯等多个学科，已经成为数据 库技术发展的一个新方向。 c t c s - 3 级列控系统是安全苛求系统，必须具有较高的安全等级。而r b c 是 c t c s 3 级列控系统中核心的地面设备，其利用数据库提供的线路数据而生成的 m a 是列车在其管辖区域安全行车的凭证，相对应的对无线闭塞中心数据库设计的 安全性、合理性要求比较高。 1 2 2数据库开发方法 随着软件工程的不断发展完善，软件研究人员也在不断探索新的软件开发方 法。目前较为常见的软件开发方法有如下几种：p a m a s 方法、面向数据流的软件开 发方法、面向数据结构的软件开发方法、问题分析法、面向对象的软件开发方法【1 4 1 、 可视化开发方法【1 5 】、原型法【1 6 1 。 数据库开发作为软件开发的一个重要分支也对应有数据库软件的开发方法， 但总体可以归为两大类【1 7 】：一类是依靠其用户的能力，感性认识和经验的设计方 法，应用于计算机系统设计过程的独立阶段的大多数方法均属于这种；另一类是 高度形式化的设计方法，这种方法主要用于数据库设计过程中较为依赖于机器的 阶段，例如性能预测和存贮结构优化的工具。 由于形式化方法主张使用正确定义的、形式的概念框架和语言严格地和无二 4 义性地陈述问题，使得设计者可以在早期发现系统中的不一致、歧义、不完全和 错误l i 引。经过实践证明形式化方法是一种行之有效的减少设计错误、提高系统可 信性的重要途径【1 9 1 ，这也是本文采用形式化建模方法作为研究方法的主要原因。 但在实际应用中，因为缺乏有效的工具，支持面向对象开发的形式化语言 ( f o r m a ll a n g u a g e ) 在可操纵性上存在很大问题。此外，单纯的形式化语言所描述的 软件系统的形式化规范( f o r m a ls p e c i f i c a t i o n ) 的可读性较差，对于缺乏相应知识的用 户来说是不易理解的，从而很容易造成软件开发者与用户之间的误解【2 0 1 。 1 3 选题的目的及意义 本课题的研究目的主要是在研究当前各种数据库技术的基础上，以c t c s 3 列控系统仿真测试平台的搭建为实际背景，选择适合的方法和工具设计生成无线 闭塞中心数据流，使之能对无线闭塞中心在通信与控车过程中涉及到的各种信息 数据进行有效的管理，并向r b c 应用层提供实现r b c 功能必需的数据服务。 首先需要分析无线闭塞中数据库的功能需求，针对功能需求设计无线闭塞中 心数据库的整体框架结构，结合无线闭塞中心数据库的特点给出整体的设计方案， 并在此基础上进行详细设计。 其次，从数据流生成的安全角度考虑，选择合适的开发方法能在早期设计中 发现问题，明确设计内容避免需求不明确造成的代价高昂的错误，并增强设计的 重用性。同时，需要选择适合的工具来解决单纯以形式化语言描述的软件系统形 式化规范( f o r m a ls p e c i f i c a t i o n ) 可读性差，对于缺乏相应知识的用户来说不易理解的 问题。针对这一问题本文选择i - l o g i x 公司的s t a t e m a t e 作为研究工具。 再次，由于c t c s 3 级列控系统是安全苛求系统，而r b c 又是c t c s 3 级列 控系统中核心的地面设备，其利用数据流生成的m a 是列车在其管辖区域安全行 车的凭证。相应的对无线闭塞中心数据流生成的安全性、稳定性要求比较高，因 此选择适合的设计开发方法有效地解决无线闭塞中心数据流设计生成过程中的安 全性问题，减少设计错误、提高系统可信性，也是本课题的一个重要的研究内容。 c t c s 3 级列控系统是基于无线通信的列车运行控制系统，是中国列车运行控 制系统的重要组成部分。无线闭塞中心( 1 氇c ) 是c t c s 3 级列控系统的地面子系 统的关键设备。行车许可的计算及发送是r b c 的核心功能，也是列车能在装备有 c t c s 3 级列车控制系统的线路上安全快速运行的行车凭证。列车运行许可的生成 需要其他外部设备提供数据，而直接从外部系统接收到的数据不能直接为r b c 直 接应用。这就需要设计生成多种数据流准确的向r b c 应用层提供实现其功能所必 需的数据。因此研究无线闭塞中心数据流的生成是非常有意义的。同时无线闭塞 5 中心数据流在c t c s 3 级列车运行控制实现安全行车控车的功能实现上也扮演着 相当重要的角色。 1 4论文的研究内容和结构安排 本论文研究的对象是c t c s 3 级系统核心地面设备r b c 内部的无线闭塞中心 数据库，以c t c s 3 级列控系统需求规范和c t c s 3 级列控系统技术创新总 体方案为依据，以c t c s 3 列控系统仿真测试平台的搭建为实际背景，完成无线 闭塞中心数据库的设计和无线闭塞中心数据流的生成。同时论文利用形式化建模 的方法，对无线闭塞中心数据流进行形式化建模，并对建立的模型进行安全性验 证。通过对设计模型实施功能仿真和安全性验证发现在设计的应用软件中存在的 漏洞，指导进行相应的设计修改，不断的提高设计的完备性和可靠性，最终达到 验证设计符合无线闭塞中心的功能需求和安全性需求。 各章节的安排如下所示： 第一章综述。本章介绍了论文的研究背景t c s 3 列控系统的原理、组 成，并简要阐述了无线闭塞中心数据流的重要性。同时，介绍了目前国内外使用 的数据库技术和数据库开发方法，进而说明了本论文研究目的，研究方向和研究 意义。 第二章s t a t e m a t e 及其理论基础。本章首先简要介绍了本论文所采用的研究方 法一形式化建模方法，接着介绍了实时嵌入式开发环境s t a t e m a t e 的特点及其建 模语言，并说明了选择该工具的优势和原因，最后介绍了作为s t a t e m a t e 行为建模 理论基础的有限状态机理论的相关概念及其特点。 第三章无线闭塞中心数据库设计与数据生成。首先根据c t c s 3 级列控系统 的主要运营场景中r b c 需要实现的功能，分析得到无线闭塞中心数据库的功能需 求。根据需求对无线闭塞中心数据库进行结构划分，并利用s t a t e m a t e 作为平台对 无线闭塞中心数据流的设计进行建模，创建数据底层结构和数据流模型。 第四章无线闭塞中心数据流仿真验证分析。利用s t a t e m a t e 的模型验证功能， 对构建的模型进行功能性模拟仿真验证及安全性验证，并对验证结果进行分析， 为进一步的研究工作奠定良好的基础。 第五章总结与展望，对整篇论文进行了总结，并对未来的工作进行了展望。 6 2s t a t e m a t e 及其理论基础 2 1形式化方法简介 形式化方法英文的名称是f o r m a lm e t h o d s ，它是指建立在严格数学基础上的系 统开发方法【2 。逻辑、代数、自动机、图论等构成了形式化方法的数学基础【2 2 1 。 用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形 式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻画、开发 和验证系统【2 3 1 1 2 4 1 。 关于形式化方法的定义颇多，虽然说法各异，但其基本内涵是相同的。所谓 形式化方法是指“基于形式系统的开发方法一网。形式化方法的实质【2 矾，即形式 化方法是由一形式系统和语用组成，一个形式系统是二元组 ，其中，l 是 一种语言，它是由符号和描述在该语言中如何写句子的语法组成的( 或称为一种 形式记法) ，c n 是对应的关系，即在l 中字符串的映射，它是由推理规则组成的。 对于给定的语言l ，其结构 判断一个特定应答器组是否属于本r b c 的管辖范围 当r b c 收到车载带有l r b g 的信息( 如位置报告) ，可以通过调用相应的数 据应用函数，判断该l r b g 是否为本r b c 管辖区域内的。 如果已知的l r b g 的n i db g 与应答器列表中的所有应答器组的n i db g 均不一致，则证明该l r b g 不属于本r b c 管辖范围，程序返回f a l s e ，否则 进行下一步； 如果已知的l r b g 的n i dc 与应答器列表中的所有应答器组的n i dc 均不 一致，则证明该l r b g 不属于本r b c 管辖范围，程序返回f a l s e ，否则进行 下一步； 如果应答器列表中的与该l r b g 编号一致( 即n mc 和n i db g 都相同) 的 应答器组所属r b c 的编号与本r b c 编号不一致，则证明该l r b g 不属于本 r b c 管辖范围，程序返回f a l s e ，否则返回t r u e 。 判断一个特定区段是否属于本r b c 的管辖范围 当r b c 收到联锁或t c c 的列车的区段占用信息，可以通过调用相应的数据应 用函数，判断该区段是否为本r b c 管辖区域内的。 如果已知的区段编号与区段列表中的所有区段的编号均不一致，则证明该 区段不属于本r b c 管辖范围，程序返回f a l s e ，否则进行下一步； 如果区段列表中的与该区段编号一致的区段所属r b c 的编号与本r b c 编 号不一致，则证明该l r b g 不属于本r b c 管辖范围，程序返回f a l s e ，否则 返回t r u e 。 输入列车数据 当列控车载设备进入确定的工作等级c t c s 3 级后，要求司机输入控车所需列 车参数( 列车长度) 和车次号等数据，并由车载设备将此数据传送给r b c 存储， r b c 再将数据发送给c t c ，并向车载设备发送回执信息m l 。 列车数据管理：无线闭塞中心数据库需要负责存储r b c 从车载收到的列车数 据，其中包括：列车种类；列车长度；最大允许速度；载重；轴重；列车能接受 的牵引电压；气密系统；列车车次号。无线闭塞中心数据库根据车载设备发送的 列车位置报告中包含的信息，及时更新列车的列车速度、工作模式、c t c s 等级等 类车动态数据。 1 4 准备发车 司机按压“发车一键，车载设备向r b c 请求行车许可( m a ) 4 0 l 。 消息管理：无线闭塞中心数据库需要存储r b c 收到列车车载设备发送的消息 号、时间戳等，以及r b c 对应发送给列车车载设备的消息号，发送次数，对应的 时间戳等，并在收到车载的消息或向列车车载设备发送消息后更新对应的数据。 3 1 2r b c 切换 r b c 切换应采用l m c 间直接通信的方式交换r b c 切换信息。 r b c 边界 i： ；来自r b c l 的进路相关信息 ： 来自r b c 2 的进路相关信息 i一。” 一 i 请求进路信息、列车数据等 进路信息、列车控制权通报等 图3 一lr b c 切换运营场景 f i g u r e3 - 1t h eo p e r a t i o ns c e n a r i oo f r b ch a n d o v e r 在r b c 切换过程中，r b c l ( 移交r b c ) 负责向r b c 2 ( 接收r b c ) 发送切 换预告信息( 车载设备i d 、r b c 边界的应答器组i d 、列车数据等) 、进路请求信 息、切换通告信息、切换确认信息、切换取消信息。