（交通信息工程及控制专业论文）CTCS3级车地通信协议设计与验证.pdf

中文摘要 摘要：随着中国铁路事业的飞速发展，对列控系统的要求也越来越高。c t c s 3 级 列控系统利用g s m r 实现车地通信，以满足高速铁路的需求。鉴于g s m r 传输 系统不能满足列控系统的高安全性指标，车地通信协议才得以在提高其数据传输 可靠性和安全性等方面发挥作用。 论文完成了c t c s 3 级车地通信系统安全通信协议( 简称c t c s 3 级通信协议) 的设计工作。首先，依据( c t c s 一3 级列控系统总体技术方案，从两个角度分析 c t c s 3 级列控系统对车地通信协议的需求：第一，从c t c s 3 级列控系统车地设 备间的通信流程角度，分析整个列控系统对车地通信系统的需求，进而得到车地 通信协议的需求；第二，从c t c s - 3 级列控系统对g s m r 传输系统q o s 指标要求 的角度分析车地通信协议的需求。然后，根据e n 5 0 1 5 9 2 安全传输系统标准，从 安全隐患防护的角度，对c t c s 3 级通信协议提出需求。 再依据上述需求对c t c s 3 级通信协议进行设计。欧洲列控系统( e t c s ) 已 经对g s m r 通信系统的应用积累了许多经验，e t r m s 也制订了欧洲无线 ( e u r o r a d i o ) 功能接口规范，详细的描述了通信协议的设计方法。因此，对于 e u r o r a d i o 规范中可以满足c t c s - 3 级通信协议需求的功能，按照e u r o r a d i o 规范 对c t c s 3 级通信协议进行设计。在此基础上，对e u r o r a d i o 规范不能满足c t c s 3 级通信协议需求之处，进行完善与补充。这样设计的安全通信协议既实现了对现 有成果的继承，又能满足c t c s 3 级系统提出的需求，也符合相关安全规范。 由于c t c s 一3 级通信协议的功能在e u r o r a d i o 规范基础上有所修改，因此，必 须通过形式化分析的方法，在设计阶段对c t c s 一3 级通信协议功能和性能进行分 析，确保设计的j 下确性与可用性。论文选用有色p 嘶网( c p n ) 对c t c s 3 级通 信协议和e u r o r a d i o 规范同时建模，然后用c p nt o o l s 工具验证模型的状念空间特 性和其他相关性能。特别是通过两个模型的比较，验证c t c s 3 级通信协议相关性 能优于e u r o r a d i o 。最后得出结论：论文研究和设计的c t c s 3 级车地通信系统安 全通信协议满足c t c s 3 级列控系统需求，具有可用性。 关键词：安全通信协议；有色p e t r i 网；c t c s 3 级；形式化分析； 分类号：u 2 8 5 j 匕塞变通厶亟堂位逾塞 垦墨至! a bs t r a c t a b s t r a c t ：w i t ht h er a p i dd e v e l o p m e n to ft h ec h i n ar a i l w a yi n d u s t r y , t h e r e q u i r e m e n t sf o rt r a i no p e r a t i n gc o n t r o ls y s t e ma r eb e c o m i n gm o r ea n dm o r er i g o r o u s t h a tc t c sl e v e l3t r a i no p e r a t i n gc o n t r o ls y s t e mo n b o a r d t r a c k s i d ee q u i p m e n t s c o m m u n i c a t eb yu s i n gg s m ri s t of u l f i l lt h eh i g h s p e e dr a i l w a yr e q u i r e m e n t s b e c a u s et h eg s m rc o m m u n i c a t i o ns y s t e mc a n tf u l f i l lt h eh i g hl e v e l s a f e t y r e q u i r e m e n t so ft r a i no p e r a t i n gc o n t r o ls y s t e mp e r f e c t l y , w en e e dac o m m u n i c a t i o n p r o t o c o lf o ro n b o a r d t r a c k s i d ee q u i p m e n t sw h i c hc a np l a ya r o l eo nr a i s i n gt h es a f e t y p e r f o r m a n c e a n dr e l i a b i l i t yi nd a t at r a n s p f o r tr e s p e c t i nt h i sp a p e r , t h ed e s i g n i n ga n dr e s e a r c h i n go fs a f e t y r e l a t e dc o m m u n i c a t i o n p r o t o c o lf o rc t c sl e v e l3o n b o a r d - t r a c k s i d ec o m m u n i c a t i o ns y s t e m ( a b b r e v i a t i o n ： c t c sl e v e l3c o m m u n i c a t i o np r o t o c 0 1 ) h a sb e e nc o m p l e t e d i nt h ef i r s tp l a c e ，t h e c t c sl e v e l3r e q u i r e m e n t sf o rc o m m u n i c a t i o np r o t o c o lh a sb e e na n a l y z e df r o mt w o p o i n t so fv i e w ：t h ef i r s ta n g e l i s a n a l y z i n gt h et r a i no p e r a t i n gc o n t r o ls y s t e m r e q u i r e m e n t f o rc o m m u n i c a t i o ns y s t e mb a s e do nt h ec o m m u n i c a t i o np r o c e s so f o n b o a r d t r a c k s i d ee q u i p m e n t si nc t c sl e v e l3 ；，n l es e c o n da n g e li sa n a l y z i n gt h e r e q u i r e m e n t sf o rc t c sl e v e l 3c o m m u n i c a t i o np r o t o c o la c c o r d i n gt ot h eg s m - r t r a n s m i s s i o ns y s t e mq o sr e q u i r e m e n ti nc t c sl e v e l3 i nt h es e c o n dp l a c e ，a c c o r d i n g t ot h ee n 5 015 9 2s y s t e ms t a n d a r dw h i c ha b o u ts a f e t y - r e l a t e dt r a n s m i s s i o n ，s o m e d e m a n d si no r d e rt op r o t e c t i n gp o t e n t i a ls a f e t yh a z a r dh a v e b e e nm a d e n e na c c o r d i n gt or e q u i r e m e n t s ，c t c sl e v e l3c o m m u n i c a t i o np r o t o c o li sd e s i g n e d e t c sh a sa c c u m u l a t e dm u c he x p e r i e n c ei ng s m ra p p l i c a t i o n ，a n de t r m sh a sm a d e t h ee u r o p e a nr a d i of u n c t i o ni n t e r f a c es p e c i f i c a t i o n ( e u r o r a d i of i s ) w h i c hd e s c r i b e s t h em e a n so fd e s i g n i n gt h ec o m m u n i c a t i o np r o t o c o lb a s e dg s m r s ow ec a nd e s i g n c t c sl e v e l3c o m m u n i c a t i o np r o t o c o l ，a c c o r d i n gt os o m ei t e m si ne u r o r a d i of i st h a t c a nf u l f i l lt h er e q u i r e m e n t so fc t c sl e v e l3c o m m u n i c a t i o np r o t o c 0 1 a n dt h e nw ec a n o p t i m i z et h ed e s i g nr e s u l tf o rs o m er e q u i r e m e n t se u r o r a d i of i sc a n tf u l f i l l b yt h i s w a y , w ec a nm a k es u r et h a tt h es a f e t y - r e l a t e dc o m m u n i c a t i o np r o t o c o ln o to n l ya t t a c h e s t h et a r g e tt oi n h e r i ts o m ea c h i e v e m e n t sb u ta l s of u l f i l lt h er e q u i r e m e n t sf r o mc t c s l e v e l3a n ds a f e t y r e l a t e dc o m m u n i c a t i o ns t a n d a r de n 5 0 1 5 9 - 2 t h ec o m m u n i c a t i o np r o t o c o la l ei m p r o v e do nt h eb a s i so ft h ee u r o r a d i of i s ，s ow e n e e dt oa n a l y z et h ef u n c t i o n sa n dc a p a b i l i t i e so fc t c sl e v e l3c o m m u n i c a t i o np r o t o c o l b ys o m ef o r m u l i z a t i o na n a l y s i sm e a n s i nt h ed e s i g ns t a g e t h e nt h eg u a r a n t e eo f c o r r e c t n e s sa n du s a b i l i t yc a nb et a k e no u t i nt h ep a p e r , c p ni ss e l e c tt om o d e lc t c s l e v e l3c o m m u n i c a t i o np r o t o c o la n de u r o r a d i of i s a n dt h e “c p nt o o l s ”i su s e dt o v a l i d a t et h es t a t u ss p a c ef e a t u r ea n do t h e rc a p a b i l i t y e s p e c i a l l y , b yc o m p a r i n gt h e s e t w om o d e l s i tc a nb ev a l i d a t e dt h a ts o m es p e c i a lc a p a b i l i t i e so fc t c s1 e v e l3 c o m m u n i c a t i o np r o t o c o la l eb e t t e rt h a no fe u r o r a d i op r o t o c 0 1 a tt h ee n do ft h ep a p e r , t h ec o n c l u s i o ni st h a tc t c sl e v e l3o n b o a r d t r a c k s i d ec o m m u n i c a t i o ns y s t e m s a f e t y - r e l a t e dc o m m u n i c a t i o np r o t o c o l ，r e s e a r c h e da n dd e s i g n e di nt h ep a p e r , i sf u l f i l l t h er e q u i r e m e n t so fc t c sl e v e l3a n dc a nb ep u ti n t ou s e i n g k e y w o r d s ：s a f e t y - r e l a t e dc o m m u n i c a t i o np r o t o c o l ；c p n ；c t c sl e v e l3 ： f o r m a l i z a t i o na n a l y s i s ； c l a s s n o ：u 2 8 5 v 图索引 图1c t c s 3 级系统构成及接口示意图j 3 图2f s f b 2 通信系统结构模型图7 图3 欧洲无线通信系统结构1 5 图4c t c s 3 级列控系统与g s m r 的连接示意图15 幽5 安全连接建立消息时序幽1 8 图6 对等实体密钥认证过程图1 9 图7 安全信息传输消息时序图一2 2 图8 安全连接释放消息时序图2 3 图9 网络注册消息时序图2 3 图l o 安全层实体的状态转移图2 4 图l lc t c s 一3 级通信协议状态转移示意图2 8 图1 2 双序列号传递示意图3 0 图1 3c t c s 3 级g s m r 通信系统c p n 模型结构图3 4 图1 4c t c s - 3 级通信协议c p n 模型功能模块图3 5 图1 5g s m - r 通信系统传输层c p n 模璎图3 6 图1 6v c 应州层c p n 模型3 8 图l7r b c 应用层c p n 模型一3 9 图1 8e u r o r a d i o 协议v c 安全层c p n 模型图4 0 图1 9e u r o r a d i o 协议r b c 安全层c p n 模型4 l 图2 0 安全连接建立超时模块c p n 模型4 2 图2 l 通信连接故障检奄模块c p n 模型4 3 图2 2 通信连接生存原语生成模块c p n 模型4 3 图2 3 序列号合法性检商模块c p n 模型4 5 图2 4 输出消息序列号写入模块c p n 模犁一4 5 图2 5c t c s 一3 级通信协议v c 安全层c p n 模型4 6 图2 6c t c s 一3 级通信协议r b c 安全层c p n 模型4 6 图2 7 条件( 1 ) 下三种丢包率的仿真结束时间5 2 图2 8 条件( 1 ) 下三种丢包率的仿真结束时间分布图5 2 图2 9 条件( 2 ) 下三种丢包率的仿真结束时间5 3 图3 0 条件( 2 ) 下三种丢包率的仿真结_ 泶时间分布图5 3 图3l 条什( 1 ) 下三种丢包率的e u r o r a d i o 协议仿真结束时间5 5 幽3 2 条作( 1 ) 下二种丢包率的e u r o r a d i o 协议仿真结束时间分布幽5 6 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作 了明确的说明并表示了谢意。 学位论文作者鹕：恤当签字嗍加7 年厂月7 日 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 提供阅览服务，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。 同意学校向国家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学位论文作者签名： 签字日期：渺7 年6 月f 1 7 同 ：移捌 磐嗍节们7 同 致谢 时光飞逝，两年的硕士研究生时光已悄然接近尾声。这段硕士研究生生涯是 我一生中收获最大，也最为难忘的岁月。忘不了，校园里美丽的风景，每一处都 是动人的画卷；忘不了，实验室里调试程序，每一个通宵工作的夜晚；忘不了， 导师的办公桌前，那每一句谆谆教诲；忘不了，试验成功，现场那每一次热烈的 欢呼。 本论文的工作是在我敬爱的导师穆建成教授的悉心指导下完成的，穆老师严 谨的治学作风、谦和的待人态度和科学的工作方法给了我极大的帮助和影响，他 的每一句话我都将铭记在心，并使我受益终身。在此衷心感谢两年来穆建成老师 对我的关心和指导。 唐涛教授为我在实验室的科研工作，指明了前进的方向，并在百忙中抽出时 间，审阅了我的毕业论文，提出了许多宝贵意见；郜春海副教授，在学习上和生 活上都给予了我们很多的关心和帮助，在此向他们表示诚挚的谢意。 交通运输自动化研究所刘波、赵波波、马连川、张建明、王海峰、黄友能、 周达天等几位老师，都在实验室的工作过程中和生活方面给了我莫大的支持，赵 波波老师、陆启进师兄还在我论文选题、撰写等方面，给了我强有力的帮助，在 此向他们表达我的感激之情。 在实验室工作及撰写论文期间，王洪涛、李晓艳、李雁、郭文章、夏夕盛等 同学对我论文中的许多研究工作给予了热情帮助，在此一并向他们表示感谢。另 外也感谢我的家人和朋友，他们对我无微不至的关怀和理解使我能够在学校专心 完成我的学业。 本论文由国家自然科学基金项目“列车运行控制及组织的基础理论与关键技 术研究”( 项目号：6 0 6 3 4 0 1 0 ) 支持。 1 绪论 进入2 1 世纪以来，中国铁路事业进入了一个大发展时期，特别是武广，郑西， 京沪等客运专线的相继开工，标志着中国已经进入高速铁路发展的快车道。因此， 高速铁路将成为中国铁路事业发展过程中的一大亮点。 随着列车运营速度的提高，列车运行控制系统在保障行车安全，提高运营效 率方面将发挥更重要的作用。目前，我国列车运行控制系统的发展仍处于初级阶 段，缺乏系统设计，没有与国际标准接轨，且铁路信号制式繁多，用户需求定义 不充分。因此，为适应我国铁路更高的安全、快速和服务需求，增强市场竞争力， 铁路部门提出了发展适于我国国情的c t c s ( c h i n e s et r a i nc o n t r o ls y s t e m ) 系统的 策略【l 】。c t c s 系统共分为c t c s 0 级至c t c s 4 级五个等级，以适应不同的运输 昏牟 赢冰。 论文作者有幸参与了c t c s 3 级车地通信系统安全传输协议( 以下简称 c t c s 3 级通信协议) 设计与实现工作。这项工作进行过程中，应用了目前较为先 进的方法和工具，以欧洲无线系统标准为基础，参考了国内外的相关安全标准， 始终紧密结合整个系统的实际需求，最终完成设计，取得了良好的实验室应用效 果。 本章的主要内容有以下三个方面：第一，介绍论文的写作背景资料。对中国 列车控制技术的发展做一综合的介绍，其中特别介绍了论文相关的车地通信技术 的快速发展和c t c s 3 级系统整体结构；对目前应用较为广泛的模型分析工具也做 了综述。第二，对当前的安全通信协议发展状况做了较为全面的总结，为工作方 案的确定奠定了曝实的基础。第三，对论文研究目的和文章结构安排做了简单介 绍。 1 1论文研究背景介绍 1 1 1列控技术发展概述 随着列车运营速度的需求不断提高，传统的以轨道电路为代表的铁路信号系 统已经无法满足实际运营需求，采用大量3 c 技术( c o m p u t e r ，c o m m u n i c a t i o n ， c o n t r 0 1 ) 的列车运行控制系统( a t c ) 逐渐成为当前铁路信号系统的重要代表。 高速铁路的崛起和发展给世界铁路的重新振兴带来了勃勃生机，使铁路装备 技术水平跃上了一个新台阶。作为高速铁路的关键设备之一，列车速度自动控制 系统具有以下3 大特点：以车载显示为行车凭证；用速度命令代替色灯含义； 信号直接控制列车动力【2 】。 为了满足我国高速铁路列控系统需求，列控系统技术平台的确立必须做到： 有利于路网的统一，有利于调度集中统一管理【3 】。对此，铁道部在2 0 0 2 年提出发 展中国列车运行控制系统( c t c s ) ，实施引进和自主研发并举的发展战略，在消化 吸收国外先进技术的同时，实现引进设备的国产化，发展c t c s 系统【舢。整个系统 共分为五个等级。 c t c s 3 级列车运行控制系统，采用无线通信系统( g s m r ) 实现地面一列车之 间连续、双向的信息传输，是基于无线通信的列车运行控制系统。列车的间隔控 制采用固定闭塞方式，列车速度控制采用目标距离控制模式( d i s t a n c et og o ) ，轨道 电路用于检查列车占用和列车完整性，地面应答器提供测距修正的定位基准及运 行方向等信息。无线闭塞中一i 二, ( r a d i ob l o c kc e n t e r ，简称r b c ) 根据固定闭塞信息 及进路信息产生行车许可( m a ) ，并通过g s m r 传输到列控车载设备。其他与 列车运行控制有关的信息，如临时限速及线路参数等，也通过g s m - r 传输到列 控车载设备【5 】。系统构成及接口示意如图1 所示。 g s m r 车载电台和g s m r 固定网络构成无线信息传输系统，实现车地信息 传输。无线通信技术作为车地信息传输技术之一，其最大优点是可以双向连续传 输大容量信息，除用于列车运行控制外，还可用于调度指挥信息，可以满足铁路 信息化对固定设备与移动体间大容量信息交换的需要，以便实现轨道交通的综合 自动化【4 】o 无线数据通信方式用于铁路列车运行控制需要具备以下条件： ( 1 ) 很高的数据传输可靠性。采取各种容错、纠错和冗余等技术，使系统数据 传输失效率和平均无故障时问达到系统要求。 ( 2 ) 能满足列车运行控制所需信息吞吐量和实时性要求。一般高速列车的运行 速度为2 7 0 3 2 0 k m h ，在5 0 m s 内对上述两种速度所造成的距离误差分别是4 4 4 m 和2 7 8 m ，都在控制允许范围之内。假设所需传输的信息量为2 5 6 - 1 0 2 4 b i t s ，为 了满足实时控制需要，在5 0 m s 内传输这些信息，信道无误码传输速率必须达到 5 12 2 0 4 8 k b i t s 。 ( 3 ) 必须是一种故障安全传输方式，所谓故障安全传输是指由于传输设备的故 障或传输通道的噪声使传输的信息发生错误的情况下，能够极力防止倒向危险侧 信息的错误传输的一种传输方式【6 j 。 目前，g s m r 通信系统是一种符合上述要求，在列车运行控制系统中广泛采 用的无线通信方式。国际铁路联盟u i c 为满足欧洲2 1 世纪铁路一体化进程推荐 2 了欧洲铁路专用移动通信系统g s m r ( g s mf o rr a i l w a y ) ，它在g s m 蜂窝系统 上增加了调度通信功能和适合高速环境下使用的要素，能满足国际铁路联盟提出 的铁路专用移动通信的要求【6 1 。 图1c t c s 3 级系统构成及接口不意图 f i g u r e1c t c sl e v e l3s y s t e ms t r u c t u r ea n di n t e r f a c em a p g s m r 系统本质作为一种通信手段，其安全性不能满足列控系统这种安全苛 求系统的需求。因此，车载子系统中由无线信息传输模块( r t m ) 负责传输车一地 间的信息，进行两者间的会晤管理，包括链路建立、链路维持和拆除链接等管理。 此模块在任务开始时应建立通信会晤，如果安全连接偶然中断但地面设备未发出 断开连接的指令时，r t m 都应认为通信会晤仍然是建立的。r t m 检测到无线通 信中断后，应先释放安全连接，然后再重新建立( 保持通信会晤) 瞵j 。 c t c s 3 级通信协议运行于r t m 的安全层，负责管理g s m r 无线网注册，安 全呼叫，安全连接建立等安全通信相关操作，是保障车载设备与r b c 问安全通信 的重要基石。因此，其研究与设计过程必须按照安全苛求系统的设计要求进行。 1 1 2模型验证工具的发展现状 文章研究的c t c s 3 级通信协议是用于安全系统的通信协议，可将协议工程的 概念应用到设计过程中，使得设计的通信协议质量得到保证。除此之外，还应该 考虑遵守安全系统的设计规范与标准。因此，整个设计过程要经过四个步骤： c t c s 3 级通信协议需求分析，c t c s 3 级通信协议设计，形式化方法建立设 计模型，对模型进行分析，验证其满足设计需求。 形式化方法是基于数学方法来描述目标软件系统性质的- - f - j 技术。用严格的 数学符号和数学法则对目标软件系统的结构与行为进行有效的综合、分析研究和 推理，它为系统的说明、开发和验证提供了一个框架，利于发现目标软件系统需 求中的不一致性、不完整性等问题【9 j 。 形式化方法一般需要形式描述技术( f d t ) 的支持，形式化描述技术涉及模型技 术和形式描述语言( f d l ) ，而形式描述语言总是以某种模型技术为基础的 9 1 。目前 有不少常见的f d t 技术被协议设计者采用，这里介绍的四种大多基于有限状态机。 ( 1 ) s d l 语言 s d l ( s p e c i f i c a t i o na n dd e s c r i p t i o nl a n g u a g e ) 是1 9 7 6 年由i t u t 发展和标准化的 一种f d t 。它的数学模型基于扩展有限状态机( e f s m ) ，是一种高层泛用型的用于 事件驱动、实时和通信系统的描述语言，电信系统和协议是它主要应用领域中的 一个【9 】o ( 2 ) 基于扩展通信有限状态机的e s t e l l e 标准 e s t e l l e ( e x t e n d e ds t a t et r a n s i t i o nm o d e ll a n g u a g e ) 的研制由i s o 发起，丌始 于1 9 8 1 年，1 9 8 9 年己被批准为国际i s o 标准。在进行事件驱动行为建模和使用 p a s c a l 进行数据处理方面，e s t e l l e 基于扩展通信有限状态机( e c f s m ) j 里论，它 能准确描述分布式并发信息系统，尤其适用于通信协议。 ( 3 ) l o s t o s 技术标准 l o t o s ( 1 a n g u a g eo ft e m p o r a lo r d e r i n gs p e c i f i c a t i o n ) 是19 8 9 年由i s o 制定的一 种用于详细说明并发和通信系统的形式描述技术标准，是一种适应协议工程、分 布处理和并行处理技术的要求而产生的规范语言。 ( 4 ) 有色p e t r i 网 p e t r i 网( p n ) 是1 9 6 2 年c a r la d a mp e t r i 开创的一种用于并发和分伽式系统行为 描述的形式化建模技术，目前还没有国际标准，但己在分布式系统和通信协议的 规格说明、验证和性能分析方面得到了广泛的应用。其应用领域从协议、硬件、 计算机软件、嵌入式系统到柔性制造系统、用户交互和业务流程1 1 1 】，同时，从经 典p e t r i 网中派生出的多种类型p e t r i 网( 有色p e t r i 网，随机p e t r i 网等) 也都根据 4 其不同特点，用来建模和分析各种过程。 有色p e t r i 网引入数据结构和分层分解的概念，又融合了位置变迁网 ( p l a c e t r a n s i t i o nn e t s ，p t n s ) 和程序语言，使之功能更加强大。其中的p t n s 为 描述并发过程的同步提供基础，而程序语言则为数据类型定义和数据操作提供基 础。c p n s 的每个标记被附加上一个称为标记颜色的数据值，引出颜色集的概念。 同时，c p n s 中的每条弧都有一个称为弧表达式( a r c i n s c r i p t i o n ) 的文本区域，定 义各条弧上可通过的标记类型和通过条件【l 引，因而特别适合于描述通信协议模 型。 论文对c t c s _ 3 级通信协议的描述将使用c p n 语言。不仅因为它的上述特点 适合通信协议建模，还可以通过c p n 工具软件对c p n 系统模型的以下动态性能做 出分析【1 3 】 1 7 】： 可达属性：可达属性( r e a c h a b i l i t y ) 广泛应用于协议分析，是分析c p n s 系统的基本属性。将可达属性应用于协议的c p n s 模型分析中，可以找到从某一初 始状态可达的所有终端状态。如果存在从初始状态可达的任何不可靠终端状态， 则该协议将被认为是有缺陷的。 有界属性：就是一个库所中令牌( t o k e n ) 的值是否有上下界限，如果令牌 值存在不确定的边界，就证明模型中的某个状态变量是失控的。 活属性：从字面上来说就是保持可激发的状态。它用来验证模型中设计的 每个变迁是否都能被激发，可以判断设计中是否有死锁状态，也就是两个事件互 为条件的现象出现。 公平属性：就是变迁发生的频率是否平衡，对于具体设计而言的实际意义 就是各个状态的转移概率是否一致，如果某几个状态问出现频繁的转移，就可以 暴露出设计中的某些缺陷。 1 2轨道交通安全通信标准及协议发展现状 1 2 1轨道交通安全通信标准 为了保证列车运行安全，欧洲电工标准委员会( c e n e l e c ) 在i e c6 1 5 0 8 标准 ( 安全相关标准) 的基础之上，制定了一系列铁路安全相关系统开发和评估的参考标 准【1 8 】。 现代化的铁路信号及控制系统一般由多个安全相关子系统构成，负责子系统 之问安全数据交换的通信系统是安全相关系统的一个重要组成部分。欧洲电工标 5 准化委员会( c e n e l e c ) 核准的e n 5 0 1 5 9 标准是专门针对铁路信号系统中安全相 关通信而设立的，此标准为构建安全相关通信系统提出了功能和技术方面的基本 要求和设计指导。目前，我国列车控制系统应用的部分欧洲设备或系统方案涉及 到e n 5 0 1 5 9 标准建立的安全通信系统及接口协议【1 9 】。 e n 5 0 1 5 9 标准提出在安全相关设备中的数据通信必须建立安全相关通信功 能，安全功能包括安全过程( s a f e t yp r o c e d u r e ) 及安全码( s a f e t yc o d e ) 两方面内容。 从结构上讲就是在应用层与通信系统之间，建立安全相关通信层，简称安全层。 需要传输的用户数据首先经过安全层的处理，生成安全层数据报文之后再发往传 输系统；从传输系统收到的信息也先经过安全层过滤才被采用。无论传输系统采 用何种结构以及协议栈，从逻辑角度，安全相关数据在安全层由安全过程和安全 码的保护进行通信。物理上安全层的数据经过传输系统传送，所以传输系统特性 直接影响安全通信功能。e n5 0 1 5 9 标准分为两个部分f 1 9 】：e n 5 0 1 5 9 1 用于封闭传 输系统，e n 5 0 1 5 9 2 用于开放传输系统。e n 5 0 1 5 9 2 讨论的开放传输系统是节点数 量未知，具有未知、可变、不可信性等属性的，存在危险非法访问的传输系统【2 l 】。 由于车地间的空间几何关系，通常情况下，轨道交通列控系统均利用开放传 输系统进行车地问的数据通信。因此，几乎所有的列控系统安全通信协议都需要 利用e n 5 0 15 9 2 标准来规范其设计。 1 2 2轨道交通安全通信协议发展现状 鉴于安全通信系统在当代列车运行控制系统中的基础性地位，许多组织都已 经设计了安全通信协议，用于保证安全相关数据的可靠传输，这罩主要列举四个 铁路中应用的安全通信协议。 ( 1 ) e u r o r a d i o 功能接口规范 欧洲铁路运输管理系统( e u r o p e a nr a i lt r a f f i cm a n a g e m e n ts y s t e m ，简称 e r t m s ) 协会为高速铁路线定义了一批规范，传统的信号系统被无线信号所代替， 列车由地面设备通过无线信号来传输移动授权信息进行管理。e t c s 第2 级和第3 级规定了以g s m r 数字无线通信系统作为列车控制信息及其相关信息的传输平 台，因为g s m 本身不能确保数据传输的安全可接受程度，因此，一种安全协议， e u r o r a d i o ，在e r t m s 标准中被定义出来。 e u r o r a d i o 系统接口规范，应用于使用开放网络的安全相关应用进程问的通 信。其规定了车载和轨旁设备间无线通信系统安全相关信息交换过程的互联互通 性，适用于包括e t c s 2 3 级在内的列控系统【2 。规范中定义了系统结构，g s m r 车载无线电台物理接口和逻辑消息接口，通信协议状态模型与时序，消息结构等 6 j b 宝变堂厶芏蝗：t 垃盐奎绪鞋 内容，其中的一些数据域( 【f 】：拨号号码等) 门为g s m r 通信系统没计。 ( 2 ) i 穆f b 2 通信协议 f s f b ( f i a ls a f ef i e l db u s ) 是欧洲列控巨头a l s t o m 开发的等门用于实现安 全数据通信网络的软件包，现在已经发展到f s f b 2 ，它在筚一代的基础上定义为， 用于实现开放传输系统安全相关数据通信的软件包“”。f s f b 2 安全协议可以有效 防护开放传输系统中的潜在威胁。其系统结构如图2 所示。 一r 一 ：搿 淼监 f s f b 2 月 墨卜 1 鼢嚣 吲2f s f b 2 通信系统鲔构模刖幽 f i g u r e2p s f b 2 c o m m u n i c a t i o ns y s t e ms t r u c t u m f s f b 2 解决”放传输系统中通信m 题的方法是从接收方的观点柬设计保护算 法。每个接收方必须验证如下的消息特征： 发送方标1 = ( 真实性) 消息j t 确性( 完整性) 消息的f r e s h n e s s ( 时效性) 消息的1 1 - 确序列号( 序州) 所有算 上- l 漤考虑发送方接收方。埘于缚个接收疗平每个传输方向由个安 全认证。换句话说，考虑两个方向上交换安全数据的两个网络咀元，可能有两个 独立的安全进程：一个检古一个方向上数据的传输，另一个是在相反的方向，两 个都位子数据接收方。 f s f b 彪一个非常独特的 殳计思路是，采用基于3 2 位c r c 的安全编码，发送 攀絮 端身份标识号s i d 以及发送端时间戳z 通过异或运算加入到c r c 校验码，得到 f s f b 2 安全码。这种方式使s i d 和正隐形于安全编码中，也使报文真实性和完整 性验证过程统一进行。因为接收端计算出c r c 校验码之后只能从安全码中恢复出 s i d 与乇经异或运算结合在一起的信息，也只有验证出s i d 及z 之后才能完成c r c 的验证【1 9 1 。 f s f b 2 协议的安全层不会对通信驱动的选择造成影响【2 3 1 ，因此可以应用于不 同的物理层。和e u r o r a d i o 不同的是，此协议为专线通信系统设计，不需要防护潜 在恶意系统攻击。因此，未采用加密技术。 ( 3 ) p r o f i s a f e 安全通信协议 p r o f i s a f e 安全通信总线是1 9 9 8 年德国p r o f i b u s 用户组织( p n o ) 以故障安 全技术的应用为目标，开始制订的一种整体的、开放的安全通信解决方案。其通 信基础是p r o f i b u s d p ，所依据的主要标准则是i e c 6 1 5 0 8 和欧洲标准e n 9 5 4 以 及e n 5 0 1 5 9 1 2 等。1 9 9 9 年，p n o 在德国汉诺威博览会上公布了在标准p r o f i b u s 上实现主、从站之间故障安全通信的技术规范，命名为p r o f i s a f e 2 5 1 。 p r o f i s a f e 的主要特点是： 安全通信和标准( 非安全) 通信在同一根电缆上共存。 p r o f i s a f e 故障安全性建立在单信道通信系统之上，安全通信不通过冗余 电缆来达到。 故障安全措施封闭在终端模块( f m a s t e r ，f - s l a v e ) 。 采用专利s i l 监视器获得极高的安全性。 最高故障安全完整性等级为s i l 3 ( i e c 6 1 5 0 8 ) 。 ( 4 ) c s e et r a n s p o r t 安全通信协议 c s e et r a n s p o r t 安全通信协议( 以下简称c s e e 安全协议) 是a n s a l d o 旗 下c s e et r a n s p o r t 公司针对封闭传输系统设计的安全协议。主要特征为s a c e m 安 全编码及d e d r 时间标记机制【2 4 1 。s a c e m 算法是一种特殊设计的散列分组编码 算法，时间标记的d e d r 值与用户安全数据一起被进行s a c e m 编码计算，而报 文真实性信息被设置为定向连接参数作为计算公式的一部分【2 0 1 。 在消息实时性保证方面，c s e e 安全协议采用d e d r 形式的双重时间戳，周 期发送的安全数据报文在被接收端收到后，都会反馈状态信息报文。在两种报文 中都含有d e d r 双重时间戳，其中d e 表示发出报文时的发送端周期计数，d r 表示发送此报文之前发送端接收到的最近一包报文的d e 字段【2 0 】。这种形式的双 重时间戳机制，也可以称之为双序列号机制，因为数据中包含的并非收发两端的 当前时间，而是双方的运行周期号。这样的好处是不需要进行双方的时间同步操 作，但缺点是双序列号会导致时间分辨率降低。 c s e e 安全协议另一大特色是，将报文源和目的信息作为定向参数纳入 s a c e m 算法中，由于封闭传输系统的节点有限，每组发送端到接收端的组合及传 输方向