（交通信息工程及控制专业论文）基于有色Petri网的无线闭塞中心子系统切换建模与验证.pdf

中文摘要 摘要：无线闭塞中心( i m c ) 是c t c s 3 级列控系统的地面核心系统，主要实现行 车许可的下达与列车间隔控制。r b c 切换功能是r b c 系统的关键功能之一，是影 响c t c s 3 级列控系统的控制精度、效率和可靠性、安全性的重要因素。本文分析 了r b c 切换的功能需求，设计了r b c 切换的流程并对r b c 切换功能进行模块划 分；在此基础上，引入有色p 嘶网建立r b c 切换功能的顶层模型与各子模块模型， 并验证和分析了模型的功能和性能。 首先，研究了r b c 系统的当前研究现状，依据c t c s 3 级列控系统划分，得 出r b c 系统在c t c s 3 级列控系统中的重要性和研究的迫切性，分析了r b c 切换 在r b c 系统中的重要地位。 其次，根据安全苛求系统的设计要求，提出r b c 切换功能的“v 字型软件 开发框架，分析了r b c 切换的功能需求，设计了r b c 切换功能的软件流程；并 依据该需求，将r b c 切换功能划分成不同功能的子模块；根据各子模块功能，归 纳出切换过程中的重要信息。 再次，引入有色p e t r i 网对r b c 切换进行形式化建模。依据有色p e t d 网的层 次化建模方法，首先建立了r b c 系统的c p n 模型；继而针对两种不同的r b c 切 换策略，分别建立不同策略下系统的顶层模型；并根据该策略的顶层模型和功能 需求，按照切换功能的模块划分，建立了r b c 切换各子模块的完整模型；与此同 时，结合r b c 切换过程的重要信息，建立了r b c 的赋时切换模型。 最后，将c p n 的仿真分析与状态空间分析方法应用于所设计的r b c 切换模 型的验证中。以状态空间报告中的内容为依据，参照c p n 的动态属性的定义，选 取车载装备2 部车载电台切换的关键模型，验证该模型的功能并分析了r b c 切换 在不同的网络质量下的成功率；并从通信延时的角度，讨论了两种切换策略的差 异，提出该设计方案的合理化建议。 关键词：c t c s 3 级列控系统；r b c 切换；有色p e t r i 网( c p n ) ；建模与验证 分类号：u 2 8 a b s t r a c t a b s t r a c t ：r a d i ob l o c kc e n t e r ( r s c ) i st h ek e ys y s t e mo fc h i n e s et r a i n c o n t r o ls y s t e ml e v e l3 ( c t c s 一3 ) s e n d i n gm o v e m e n ta u t h o r i t y ( m a ) a n dc o n t r o l l i n g t h ed i s t a n c eb e t w e e nt r a i n sa r et h em a i nf u n c t i o n so fr b c r b ch a n d o v e ri st h eo n eo f t h ek e yf u n c t i o n so fr b cs y s t e m ；i th a sa ni m p o r t a n te f f e c to nc o n t r o l l i n gp r e c i s i o n ， e f f i c i e n c y , r e l i a b i l i t yo fc t c s 3 i no r d e rt oi m p r o v er e l i a b i l i t yo ft h ee n t i r er b c s y s t e m ，t h i sp a p e ra n a l y z e dt h ef u n c t i o n a lr e q u i r e m e n to fr b ch a n d o v e r , d i s c u s s e dt h e f l o wo fr b ch a n d o v e ra n dc o m p a r t m e n t a l i z e dr b ch a n d o v e rf u n c t i o nt os e v e r a lp a r t s o nt h i sb a s i s ，e s t a b l i s h e dt h et o pm o d e la n da l ls u b - m o d e l so fr b ch a n d o v e rb y c o l o r e dp e t r in e t ，f i n a l l yv e r i f i e dt h ef u n c t i o n sa n d c a p a b i l i t yo f t h em o d e l f i r s t l y , r b cs y s t e mr e s e a r c hs t a t u sw a sd e s c r i b e di n t h i sp a p e r , g a i n e dt h e s i g n i f i c a n c ea n di m p e n d e n c yo fr b c i nc t c s 一3t r a i nc o n t r o ls y s t e md e p e n d i n go n c o m p a r t m e n t a l i z i n go fc t c s 一3 ，t h ei m p o r t a n c eo fr b c h a n d o v e rw a so b t a i n e dw i m t h eh e l po fs u c ha n a l y s i s s e c o n d l y , t h e ，v s h a p ed e v e l o p e ds t r u c t u r eo fr b c h a n d o v e rf u n c t i o nw a sg i v e n b a s e d0 1 1t h er e q u i r e m e n to fs a f e t yi n t e g r i t yl e v e l ，a n dt h e nt h ef l o wo fr b ch a n d o v e r s o f t w a r ew a sd e s i g n e d i na d d i t i o n a l ，t h i sp a p e rd i v i d e dr b ch a n d o v e rf u n c t i o n si n t o s e v e r a lp a r t sa c c o r d i n g 勰r b ch a n d o v e rr e q u i r e m e n t t h ei m p o r t a n ti n f o r m a t i o no f r b ch a n d o v e rw a sg i v e n t h i r d l y , c o l o r e dp e t r in c tw a su s e dt om o d e lt h er b ch a n d o v e rp r o g r e s s a c c o r d i n gt oh i e r a r c h i c a lc p n ，t h i sp a p e rs e tu pr b cs y s t e mm o d e l ，a n db e c a u s et h e r e h a st w od i f f e r e n tt a c t i c st oc o m p l e t er b ch a n d o v e rf u n c 6 0 玛s ot w od i f f e r e n tt o p m o d e l sw e r ee s t a b l i s h e d b a s e do nt h ef u n c t i o n a lr e q u i r e m e n t sa n dp a r t i t i o n , a l l s u b m o d e l sw e r ee s t a b l i s h e dp a r t i c u l a r l y a tt h es a m et i m e ，c o m b i n i n gw i t ht h e i m p o r t a n ti n f o r m a t i o n ，t i m e dc p nm o d e l so fr b ch a n d o v e rw e r ee s t a b l i s h e da sw e l l b e c a u s eo ft i m ei n f l u e n c e f i n a l l y ，o nt h eb a s i so ft h em o d e l s ，t h es t a t es p a c ea n a l y s i sa n ds i m u l a t i o na n a l y s i s w e r eb r o u g h tf o r w a r dt oa n a l y z ea n dv a l i d a t et h ea p p l i c a t i o ns o f t w a r eo fr b ch a n d o v e r 硼1 cm o d e lo f2m t 2e q u i p p e df o ro n b o a r dw a sc h o s e nt ob es e r i o u s l ys t u d i e d t h e f u n c t i o n a lv e r i f i c a t i o na n ds a f e t ya n a l y s i so ft h i sm o d e lc a r r i e do u tb yt h em e t h o do f s t a t es p a c ea n a l y s i s t h es u c c e s s f u lr a t eo fr b ch a n d o v e rw a sg i v e nu n d e rd i f f e r e n t g s m - rn e tq u a h t y t h ed i f f e r e n tp e r f o r m a n c e sb e t w e e nt w oh a n d o v e rs t a t i c sw a s d e s c r i b e do nt h eb a s eo fc o m m u n i c a t i o nd e l a y s o m ea d v i c eo fi m p r o v e m e n tt ot h e p e r f o r m a n c ew a sg i v e n a tl a s t k e y w o r d s ：c t c s - 3 ；r b ch a n d o v e r ；c p n ；m o d e l i n g ；v e r i f i c a t i o n c l a s s n o ：u 2 8 v 图索引 图lr b c 与其他设备接口2 图2r b c 切换软件开发框架8 图3 安全计算机平台的结构l o 图4r b c 切换1l 图5r b c 切换流程图1 3 图6r b c 主要功能1 4 图7r b c 切换功能模块细化1 5 图8r b c 子系统顶层模型一2 0 图9 车载装备l 部m t 2 的切换流程。2 2 图l o 车载装备l 部m t 2 的顶层模型2 2 图l l 车载装备2 部m t 2 的步骤j 2 3 幽1 2 车载装备2 部m t 2 的顶层模型2 4 图1 3 列车最大安全前端到达切换预告点的模型2 5 图1 4 混合m a 计算模型2 6 图1 5 列车最大安全前端到达切换点的模型2 7 图1 6 列车最小安全后端到达切换点的模型2 8 图1 7 移交r b c 的列车管理模型3 l 图1 8 接管r b c 的列车管理模型3 3 图1 9 相邻r b c 交互模型一3 5 图2 0 车载装备1 个m 他的赋时模型3 7 图2 l 车载装备2 个m t 2 的赋时模型3 8 图2 2 模型检验过程4 2 图2 3 模型仿真运行图( 一) 一4 4 图2 4 模型仿真运行图( 二) 4 5 图2 5 模型仿真运行图( 三) 一4 6 图2 6 模型状态空间可达图4 7 图2 7 模型2m t 2 的状态空间信息4 8 图2 8 模型2m t 2 的状态空间有界性4 9 图2 9 模型2m t 2 的状态空间多重集属性( 上界) 5 0 图3 0 模型2m t 2 的状态空间多重集属性( 下界) 5 0 图3 l 模型2m t 2 状态空间家态性5 l 图3 2 模型2m t 2 的状态空间活性5l 图3 3 模型2m r 2 的状态空间公平性( 一) 5 2 图3 4 模型2m 1 2 的状态空间公平性( - - ) 5 2 图3 5 切换成功率和网络质量关系5 4 图3 6 车载装备2 部m t 2 时的通信延时对切换时间的影响一5 5 图3 7 车载装备1 部m t 2 时的通信延时对切换时间的影响5 5 6 1 表索引 表l 列车状态标志位含义说明1 6 表2r b c 系统模型的库所说明2 0 表3r b c 系统模型的变迁说明2 l 表4 两种切换策略的库所说明2 9 表5 两种切换策略的变迁说明。2 9 表6 移交r b c 的列车管理模型库所说明。3 2 表7 移交r b c 的列车管理模型变迁说明_ 3 2 表8 接管r b c 的列车管理库所说明3 3 表9 接管r b c 的列车管理模型变迁说明。3 4 表1 0 相邻r b c 交互模型库所说明3 6 表l l 相邻r b c 交互模型变迁说明3 6 表1 2 赋时模型的库所说明3 8 表1 3 赋时模型的变迁说明。3 9 表1 4 网络质量和切换成功次数对应表5 4 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作 了明确的说明并表示了谢意。 靴做储戤：斜 签字日期：秒“月夕日 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国 家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学位论文作者签名： 签字醐：年 导师签 签字日期日 卞7 鸯月 ，o 致谢 衷心感谢我的导师郜春海教授! 本文的工作是在郜老师悉心指导下完成的。 郜老师渊博的知识、严谨的治学态度，敏捷的思维和一丝不苟的钻研精神给了我 学业上很大的帮助。他的人格魅力也深深的影响着我，他所倡导的勤于思考、敢 于创新的精神将使我受益终生。在此，衷心的感谢他两年来对我的教诲，以及生 活上的关心和帮助。 感谢轨道交通控制与安全国家重点实验室唐涛老师，在他的指导下加深我对 问题认识的深度和广度。感谢刘中田、王海峰、马连川老师指导我参与科研工作， 他们的帮助使我的科研能力有了很大的提高。在此向他们表示由衷的谢意。 感谢实验室的刘波、张建明、周达天、徐田华、黄友能、燕飞老师对我论文 的耐心指导并提出的宝贵意见和建议。借此向他们表达我深深的感激之情。 在实验室撰写论文期间，感谢吕继东、陈磊、陆启进、杨旭文等师兄对我论 文研究工作的帮助和指导。感谢程梁、梁楠、杨扬、秦岭、李伟、王观宁、贺广 字、孙伟、刘丽娟、李凯、耿鹏等同学给予我论文的许多很好的建议。也要感谢 张庆新、李子钧、李雷等师弟师妹们给我的热心帮助。 非常感谢我的家人对我的支持和帮助，在漫长的求学生涯中，他们的无限关 怀和鼓励使我能保持乐观的心态和不断地进步。尤其要感谢我的母亲，她给我无 微不至的关怀是我前进路上动力所在。 最后，衷心的感谢各位参与论文评阅和答辩的评委老师和专家学者，感谢你 们的辛勤劳动和宝贵意见! 本论文由国家自然科学基金项目“列车运行控制及组织的基础理论与关键技 术研究( 项目号：6 0 6 3 4 0 1 0 ) 支持。 1 综述 1 1r b c 系统研究现状 随着铁路大提速、客运专线和青藏铁路等跨越式发展举措的实施，我国铁路 进入了快速蓬勃发展的关键时期。参考欧洲列车控制系统e t c s ，我国在2 0 0 2 年 提出了适合我国国情的中国列车控制系统( c t c s ) ，它是中国铁路为了保证列车 安全运行，并以分级形式满足不同线路运输需求的技术规范。c t c s 分为5 个应用 等级【l 】：c t c s0 级、c t c s1 级、c t c s2 级、c t c s 3 级、c t c s 4 级。目前正在研 究c t c s3 级的关键技术和标准。 c t c s 3 级是基于无线传输信息、采用轨道电路等方式检查列车占用的列车运 行控制系统。面向提速干线、高速新线或特殊线路，采用基于无线通信( g s m r ) 的固定闭塞或虚拟自动闭塞。 c t c s 3 级列控系统包括地面设备和车载设备两大部分： 1 ) 地面设备由无线闭塞中心( r a d i ob l o c kc e n t e r ，r b c ) 、列控中心( t c c ) 、 联锁设备( c i ) 、z p w - 2 0 0 0 ( u m ) 系列轨道电路、应答器( 含l e u ) 、 g s m r 通信接口设备等组成； 2 ) 车载设备由车载安全计算机( v c ) 、g s m r 无线通信单元( r t u ) 、轨道 电路信息接收单元( t c r ) 、应答器信息接收模块( b t m ) 、记录单元 ( d r u ) 、人机界面( d m i ) 、列车接口单元( t ) 等组成。 r b c 作为c t c s 3 级中的重要组成部分，是地面设备的核心。r b c 负责与车 载设备之间通过g s m - r 网络完成大容量连续双向的车地信息交互，是整个c t c s 一3 级列车控制系统的核心功能，通过信息交互实现了r b c 对运行列车的控制，从而 实现c t c s 3 级列控系统的主要功能。 r b c 主要功能包括：无线通信管理、列车数据管理、行车许可管理、r b c 切 换管理、本地维护终端、线路数据管理和车载模式管理等。r b c 通过与其他设备 间的接口获得有效数据，并通过自身软件的处理，完成r b c 对列车安全行车的管 理。 r b c 与其他设备的接口关系如下图所示： 图1r b c 与其他设备接口 f i g u r e1i n t e r f a c eo fr b c 鉴于r b c 在地面列控系统中所起的重要作用，很多世界知名列控生产厂家纷 纷投入r b c 的研究中，并采用各自不同的设计框架，得到功能不尽相同的产品， 部分产品也取得了一定的成绩，主要有c s e e 公司和g e 公司的r b c 产品。 1 ) c s e e 的r b c 设备【2 j 采用c s e e 运输公司的安全计算机结构( 三取二结构) ，使得r b c 系统 具有很强的安全性和可用性。接口上使用标准的安全通信协议( e u r o r a d i o ) 通过g s m r 网络或并行接口实现连接。用g s m - r 、安全计算机及网络接口 以完全冗余的方式监控列车。主要功能有：( 1 ) 列车识别与定位；( 2 ) 列车 控车模式监督；( 3 ) 向被控的列车发送移动授权( m o v e m e n t a u t h o r i t y ，m a ) 。 该产品应用于马德里至雷里达线上。 2 ) g e 的r b c 设备【3 】 增强型列车控制系统( i t c s ) 将全线划分为若干控制区，每个控制区包 括几个车站和区间，由一个r b c 控制。r b c 将控区划分为若干个无线闭塞分 区。无线闭塞分区的划分，与原有的自动闭塞重合。地面设备包括r b c 、r b c 远端模块、g p s 差分站、无线电台以及始端站r b c 。g e 的r b c 是基于安全 计算机的控制系统，主要功能有：( 1 ) 本控制范围内的列车控制；( 2 ) 配置 数据库，实现无线闭塞；( 3 ) 与c t c 设备接口，接收并执行临时限速命令； ( 4 ) 与联锁接口，采集所在车站进出站信号机状念及道岔正反位状态信息。 该系统目前正在装备于底特律到芝加哥全线。 2 1 2p e t r i 网建模语言应用现状 形式化方法( f o r m a lm e t h o d ，f m ) 是一种用于规范、设计和验证计算机系统 的基于数学的方法，包括各种语言、技术和工具等1 4 1 。它使用严格的数学方法和数 学符号对目标系统的结构与行为进行有效的分析研究和推理，为系统的开发和验 证提供了一个框架，有利于发现目标系统中的不完整性、一致性等问题【州。 形式化方法包含两个重要研究内容：形式化规范，它是对软件完成什么功能 的数学描述，是用具有精确语义的形式语言书写的系统功能描述；形式化验证， 它是指使用严格的数学方法来推理验证产品或设计是否符合其全部或部分规范的 过程。 有色p e t r i 网( c o l o r e dp e t r in e t ，c p n ) 是形式化的方法之一，能够将系统用 图形化的方法精确表示出来，并且提供可视化分析，这就使得复杂系统变得容易 理解，从而能更清晰的掌握系统的各种信息。因此也更易于发现系统的缺点【7 j 。 1 2 1 有色p e t r i 网概述 p e t r i 网是一种系统的数学和图形的描述与分析工具，由德国科学家c a r la d a m p e t r i 在1 9 6 2 年提出【8 1 。p e t r i 网分析方法和技术既可以用于静态的结构分析，又可 以用于动态的行为分析，特别适用于具有并发、异步、分布、并行、不确定性的 信息处理系统。经过几十年的发展，p e t r i 网理论得到了极大的丰富，其应用己经 涉及计算机学科的各个领域，如线路设计、网络协议、软件工程、人工智能、形 式语言、操作系统、并行编译、数据管理等 9 1 。 p e t r i 网的定义如下【l o j ： 定义1 1 三元组n = 【s ，t ，f ) 称为有向网的充分必要条件是： ( 1 ) snt = ；( 2 ) su r 矽；( 3 ) f 心x 丁) u 仃s ) ( “ 为笛卡尔积) ； ( 4 )a o m ( r ) u c o d ( r ) - - s u t ， 其中d o m ( f ) = b l3 y ：g ，j ，) f ， c o d ( f ) = yi3 x ：b ，y ) f j 。 其中s 和t 分别称为n 的库所( p l a c e ) 集和变迁( t r a n s i t i o n ) 集，f 为流关 系( f l o wr e l a t i o n ) 。x = s u t 称为n 的元素集。库所( 又称s 元素) 集和变迁( 又 称为t 元素) 集是有向网的基本成分，流关系是从它们构造出来的。库所和变迁 是两类不同的元素，所以s n 丁= 其交集为空；s u t 表失望中至少要有一个 元素，每个库所代表一种资源，资源的流动由流关系规定，所以变迁只能与库所 有直接的流关系；f p x 丁) u 仃s ) 表明不参与任何资源变迁的库所表现为鼓励 的库所，不引起任何资源流动的变迁表示为孤立的变迁；d o m ( f ) uc o d ( f ) = su t 3 规定网中不能有孤立元素。 一个p e t r i 网模型的动态行为是由它的实施规贝i j ( f i r i n gr u l e ) 来规定的。当一个 变迁的所有输入库所至少包含一个标记( t o k e n ) 时，这个变迁才能实施。其实施 后的结果就是从它所有的输入库所中减去一个标记，并在其输出库所中产生一个 标记。 有色p e t r i 网c p n ( c o l o r e dp e t r in e t ) 是由丹麦的j e n s e nk u r t 在基本p e t r i 网基 础上定义的一种高级网系统。比起基本网系统，这种高级网系统更抽象：每个库 所( p l a c e ) 上均能有多种资源，每个变迁( t r a n s i t i o n ) 上都能代表多种变化，从而使用 起来结点少，便于把握。c p n 特别适合于对通信协议、分布式系统、自动生成系 统、工作流程进行分析和建模【i l l 。同时，c p n 作为一种高级p e t r i 网，被认为是基 于网络复杂系统建模和分析的最佳工具，用它建立的模型是可执行的，有利于动 态仿真。c p n 不仅具有普通p e t r i 网描述并发、同步、异步、资源竞争、协调等离 散事件动态系统行为的功能，而且结合高级编程语言和建模的层次结构，能够完 成包含复杂数据类型定义和数据处理的大型系统建模【1 2 1 。 有色p e t r i 网定义【1 3 】如下： 定义1 2 ：c p n 可行实话定义为多元组c p n = ( ，只r ，a ，n , c ，g ，e ，) ，其中： 1 ) 是类型( t y p e s ) 的非空有限集，也称为颜色集( c o l o rs e t s ) ； 2 ) p = 扫。，p ：，a ，p 。) 是库所的有限集，m 表示系统中库所的数目； 3 ) t = t ，t 2 ，a ，t 朋 是变迁的有限集，n 表示系统中变迁的数目； 4 ) 彳是弧( a r c ) 的有限集，满足p nt = p f 7a = t na = 0 ； 5 ) 节点( n o d e ) 函数，定义为一p x t u t p ； 6 ) c 是颜色( c o l o r ) 函数，定义为c ：p _ ； 7 1g 是哨( g u a r d ) 函数，也可以称为变迁表达式函数，定义为 g ：t 专e x p r e s s i o n s ，满足：v t t ：阢e ( g ( f ) ) = bar y p e ( v a r ( g ( t ) ) ) j 。 其中，t y p e ( v ) 表示变量类型，v a r ( e x p r ) 表示表达式e x p r 的变量集。 8 1e 为弧表达式( a r ce x p r e s s i o n ) 函数，定义为e ：a 哼e x p r e s s i o n s ，满足： v t t ： t y p e ( e ( a ) ) = c ( pm sat y p e ( v a r ( e ( a ) ) ) 】，其中p 为 ) 中的 库所，c ( p ) m s 表示居于c ( p ) 之上的所有多重集的集合，以下类同。 9 ) j 是初始化( i n i t i a l i z a t i o n ) 函数，定义为i ：p c l o s e d e x p r e s s i o n s ，满足： 坳p ： t y p e ( i ( p ) ) = c 切m sj 。 1 2 2p e t r i 网在铁路系统中的应用现状 1 ) 时间p e t r i 网在铁路专家系统建模中的应用【1 4 】 4 时间p e t r i 网是在变迁集上带有时间约束的一类p e t r i 网。铁路科学研究院以铁 路智能运输系统( r i t s ) 为研究背景( r i t s 中的核心问题均面临时间知识的处理 问题，要求有高效的时间知识处理算法) ，利用基于时间p e t r i 网的结构特性优良、 分析性能好的特点，引入模糊时间区间的操作，在基于系统的时间知识p e t r i 网模 型的基础上构建了相应的时间知识系统的生成图，用生成图进行时间知识验证和 推理。该算法能处理不确定的时间区间，具有效率高、可处理时间区间的不确定 性问题等优点。同时，利用这种算法可验证时间约束列车运行调整方案的可行性， 能验证铁路专家系统中时间知识的一致性，用算法的生成图可推导出某些时间约 束事件同时发生的可能性，直接求出和某事件发生的相关事件发生的时间推理。 文献【1 4 1 中提出的办法较好地解决了知识获取的问题。 2 ) c p n 用于e t c s 建模 德国铁路( d e u t s c h eb a h n a g ) 和不伦瑞克技术大学控制与自动化工程学院以 e r t m s e t c s 规范为基础提出了一种形式化模型【1 5 】。一共包括三个子模型：环境 模型、车载系统和轨旁系统。不同的操作和过程以脚本的形式被可视化，脚本被 进一步细化为功能。而且提出了用p e t r i 网作为所有开发阶段的形式化描述方法， 并用d e s i g n c p n 作为支持工具。 针对用c p n 建模工具d e s i g n c p n 建立的e t c s 系统模型，是一个复杂的分 布式自动系统，提出了在模型建立和运行仿真中的一些技术问题【1 6 】。列车控制系 统的建模开始于不同的建模范例，在e t c s 的建模中，综合了三个不同的建模方 面：组件( c o m p o n e n t s ) 、脚本( s c e n a r i o s ) 和功能( f u n c t i o n s ) 。对组件进行建模时，重 点是不同子系统之间的通信和交互；从脚本特性看，是对操作程序进行建模，主 要是车载设备与轨旁设备之间的交互以及维持操作所要求的事件序列。个别的脚 本连接成组并以这种方式形成组件。在较低的模型层上是功能模型描述，功能模 块可以用在不同的对象中。 3 ) 有色p e t r i 网对联锁系统建模【r 7 】 同济大学利用包含层次结构的有色p e t r i 网，利用层次化的方法将车站信号联 锁逻辑分为联锁逻辑关系层和联锁设备层，并且在车站联锁设备层面进行了形式 化描述，使得联锁系统这样的复杂系统的形式化结构清晰，有利于分析和计算机 处理。 1 3 选题目的和意义 c t c s 2 级是目前现有的列车控制系统，是基于点式应答器、连续轨道电路传 输列车运行控制信息的点连式列车超速防护系统，已经在提速线路和客运专线获 5 得成功应用，适用于2 0 0 k m h - 2 5 0 k m h 的线路。但是，该系统还存在如下可以改 进的方面：地面设备和线路检查设备沿铁路全线分布，设备投资高，维护成本大。 尤其是一些地理环境恶劣的区域，维护的困难很大。列车在站间反向运行时，只 能采用自动站间闭塞，列车不能追踪运行，影响运行效率。目前的z p w 2 0 0 0 轨道 电路最多只能显示前方七个闭塞分区空闲，难以支持3 5 0 公里以上时速的高速列 车运行需要。铁路沿线地面设备过多，地面向列车传送信息的信息量不足、实时 性不够，车地之间不能实现双向通信，这是我国铁路控制系统亟须解决的问题。 针对上述问题，一个很好的解决方案就是尽量减少地面设备，采用无线传输 方式来实现车地之间的双向、大容量、实时的信息传递，于是r b c 作为解决这些 问题，实现高效率的铁路运输的解决方案出现了，研究r b c 系统构成及其关键 技术的也变得意义重大。 r b c 是一个非常复杂的安全计算机系统，它对于系统的安全性和可靠性有着 极高的要求，直接关系到铁路行车安全和人民生命财产安全。其硬件设计时采用 2 2 0 0 2 的热备配置等方式提高可靠性，而在应用软件设计方面，需要严格分析其 功能需求，按照安全苛求系统的要求进行设计，因此对应用软件的可靠性和完备 性要求很高。 在r b c 的各个功能中，r b c 切换作为r b c 的主要功能之一，是影响c t c s 3 级列车运行控制系统的控制精度、效率和可靠性、安全性的重要因素，高速铁路 中应用c t c s 3 级时，r b c 控制区域一般约7 0 k i n ，列车以3 0 0 k m h 行驶时每隔1 4 分钟左右就需要进行一次切换【l 钔，如果切换时间过长则会使得列车在运行至r b c 边界的时候减速运行，将大大影响了行车效率；如果切换失败，列车将转入c t c s - 2 级运行，这将对运行效率产生严重的不良影响，并且浪费资源。更为严重的是， 这种后果将使得r b c 系统的可靠度与安全性降低。 1 4 研究内容与组织结构 本论文是在c t c s 3 级系统中对r b c 子系统切换进行研究分析，首先研究了 r b c 切换功能需求和设计，并对切换过程进行模块化分，进而分析得出r b c 切换 中的重要参数和影响因素，在此基础上利用有色p e t r i 网( c p n ) 进行建模，并对 模型进行功能验证和性质分析，然后在模型功能完备的基础上定量分析r b c 切换 过程中关键因素影响，并最终得到在不同的切换策略下r b c 的切换时间对比分析。 各章节的安排如下： 第一章综述，说明了目自订国内外的列车控制系统中的r b c 子系统的丌发及 应用现状，并介绍了形式化方法p e t r i 网理论和p e t r i 网在列控系统中的应用状况。 6 提出了论文目的及意义。 第二章r b c 切换功能软件设计，首先阐述了r b c 切换功能的软件设计结构， 并根据安全苛求系统的设计要求，给出r b c 切换功能的软件设计“v 字型开发 框架，然后依据r b c 切换功能需求设计r b c 切换的具体流程，并依据流程将r b c 切换功能划分成不同的子功能模块，在此基础上分析指出切换过程中的重要信息。 第三章基于c p n 的r b c 切换建模，在完成对系统的功能需求分析的基础上， 按照c p n 的层次化建模方法，建立不同r b c 切换策略的顶层模型，并对顶层模 型细化至子网模型，然后根据r b c 切换的功能模块化分建立各模块的详细模型， 并依据切换过程的重要指标，建立r b c 切换的赋时模型。 第四章基于c p n 的r b c 切换功能验证与分析，在模型的基础上利用c p n 的 动态分析方法对r b c 切换过程的模型进行了功能验证和安全性分析。分析了在不 同的网络质量下r b c 切换的成功率，并从通信延时的角度上，比较分析了两种切 换策略的差异，得出合理的切换建议，提高这一过程的安全性和可靠性。 第五章研究工作总结和展望，对整篇论文做出总结，并对今后的工作进行了 展望。 7 2r b c 切换应用软件设计 软件设计是一个用代码陈述需求的过程。这种陈述得出一个对软件的全局观 点。系统通过逐步求精使得设计陈述逐渐接近源代码。有两个基本步骤；第一步 是初步设计( p r e l i m i n a r yd e s i g n ) ，关注于如何将需求转换成数据和软件框架。第 二步是详细设计( d e t a i ld e s i g n ) ，关注于将框架逐步求精细化为具体的数据结构 和软件的算法表达。 r b c 系统是基于安全计算机平台构建的。是基于故障安全原则设计的控制系 统，主要功能是处理从地面系统接收的信息以及与车载设备子系统交换信息，交 互的信息是通过g s m r 网络进行传输的安全数据。 r b c 切换是r b c 系统中的重要功能之一，保证了列车在通过相邻r b c 边界 时能够安全、顺利的通过。按照目前r b c 的布置原则，高速列车在行驶时，r b c 切换时间间隔很短，因此，保证这一过程的安全性、可靠性是十分重要的。 2 ir b c 切换设计框架 由于r b c 系统是安全苛求系统，按照安全苛求系统的要求，建立r b c 切换 功能软件的设计框架，它是一个“v 字型图，如图2 所示。描述了r b c 切换软 件开发过程的步骤，各阶段严格按顺序进行，每一阶段的工作成果都必须经过评 审确认无误后才能进入下一阶段。在实践中，经常有这种情况：在开发和测试期 间发现，软件开发工作需要进一步的设计工作、更加明确的需求或者更加清楚的 问题说明，开发过程需要返回到前面的阶段。 软件需求分析 ( 功能、性能) 系统调试 验证和测试 萋篥蓑磊鳖 巨 详细设计 模块化r 一一一 兰- 堑一。墅j 萎，茎冀， f 1 _ l * ， 功能验证 详细设计文档产童i 编码 图2r b c 切换软件开发框架 f i g l l 他2f r a m e w o r ko fr b ch a n d o v e rs o f t w a r e 系统溅试 软件需求分析阶段包括对r b c 切换功能软件的功能需求分析和性能需求分 析，需求分析在整个软件开发周期中是非常重要的，因为它是软件设计的基础。 好的需求分析可以减少甚至避免软件开发中的错误和遗漏，缩短开发周期，提高 软件质量。 软件设计阶段包括概要设计和详细设计。这一部分对软件完成功能的详细过 程和功能进行设计，提供下一阶段的编码的效率。编码过程不是本文的研究重点， 因此不做讨论。 形式化建模是利用有色p e t r i 网对r b c 切换软件按照设计进行提炼，建立模型 用于仿真分析和验证软件的功能，这个过程反映了r b c 切换过程的实质，并且有 利于的发现设计中存在的问题， 用有色p e t r i 网建模后，可以对r b c 切换软件的功能和性能通过c p nt o o l s 的方法进行验证。对模型中的各个状态进行分心，反映系统的各项属性。 2 2r b c 切换功能需求分析 安全性需求和功能需求可以统归为r b c 切换应用软件的需求分析，这个阶段 是非常重要的，其中的失误会给整个r b c 系统的应用软件的开发带来很多麻烦和 损失。这个阶段的主要任务是明确r b c 切换应用软件的安全性和功能需求需求。 2 2 1i m c 切换安全- 性需求 r b c 切换是r b c 系统应用软件的一个重要组成部分，它随整个r b c 系统其 他应用软件一起，构建于安全计算机平台f 1 9 1 之上。r b c 是c t c s 3 级列控系统的 重要组成部分，与其他地面设备接口众多。其可靠性关系到整个运行线路的通畅 和行车的安全，如果因为故障导致列车停运或是系统瘫痪，甚至严重的事故，所 造成的损失是不可估量的。因此对r b c 的可靠性有着非常苛刻的要求，要求r b c 能够保证系统安全、可靠、连续的运行。 在硬件方面，安全计算机平台通过硬件的容错、安全结构设计和与其配合的 平台软件来实现安全相关功能。r b c 对于安全计算机平台而言只是构建于v x w o r k s 实时多任务操作系统之上的安全计算机平台软件之上的应用软件( 任务) 。安全计 算机平台的容错、安全处理过程对于r b c 设备的应用流程透明。为了满足c t c s 一3 级列控系统对于安全完整性等级【2 0 1 ( s i l ) 的要求，安全计算机平台从硬件设计上 采用了2 2 0 0 2 结构，从最大程度上保证数据的准确性以及列车运行的安全，并在 保证了r b c 应用程序在安全计算机平台上运行出现某些问题时能够维持整个系统 9 e 立套适厶= i 兰熊竺监监塞 b b 如拯应山丝址瞠吐 的l f 常l 作。 硬件基本结构如下图所示 以太阿 圈3 安全计算机平台的结构