（交通信息工程及控制专业论文）CBTC区域控制系统中列车管理的建模与分析.pdf

中文摘要 摘要：随着无线通信技术的飞速发展，无线通信的可靠性、可用性大大提高， 基于通信的列车运行控制系统( c o m m u n i c a t i o nb a s e dt r a i nc o n t r o ls y s t e m ，c b t c ) 成为当今轨道交通列车运行控制系统的发展趋势。c b t c 系统是连续的自动列车控 制系统，它通过高精度的列车定位技术和不间断的车地通信，通过提供更精确的 列车控制、持续的列车安全分隔和超速防护，使得列车可以在更短的运行间隔内 实行安全运行。 在c b t c 系统中，轨旁设备区域控制中心在保证列车安全运行方面发挥着重 要作用，它能够实时的与其它子系统进行进行交互，通过为列车提供移动授权来 管理列车的运行。因此区域控制中心对于列车进行合理的安全的管理具有非常重 要的意义。 本文从研究区域控制中心的列车管理入手，依照系统功能需求，从结构、状 态和流程等多角度详细阐述了列车运行管理的原理。根据管理列车的目的重点介 绍了多车运行管理的具体过程。 本文采用基于层次时间有色p e t d 网的形式化建模方法，分析了系统建模的可 行性并对区域控制中心列车管理过程构建了顶层，数据信息交互层和m a 计算层 的三层模型。在对系统模型进行改进与简化的基础上对模型予以仿真运行，通过 基于状态空间的分析方法从不同角度验证了模型设计的合理性与数据传输的正确 性，有助于构建功能更加完善的区域控制中心系统模型，也为区域控制中心系统 的软件实现提供了理论依据。 关键词：c b t c ；区域控制中心；列车管理；c p n 建模 分类号：u 2 8 4 4 4 a b s t r a c t a b s t r a c t ：a c c o m p a n y w i t ht h ep r o g r e s so f w i r e l e s sc o m m u n i c a t i o nt e c h n o l o g y ，t h e r e l i a b i l i t y a n d a v a i l a b i l i t y o fw i r e l e s sc o m m u n i c a t i o na r eh i g h l yi m p r o v e d c o m m u n i c a t i o nb a s e dt r a i nc o n t r o l ( c b t c ) h a sb e c o m et h et r e n do fu r b a nr a i l w a y t r a f f i cc o n t r o ls y s t e mi nm o d e r nt i m e s c b t cs y s t e mi si n d e p e n d e n to f r a i l w a yc i r c u i t ， a p p l y i n gh i g hr e s o l u t i o nt r a i nl o c a t i o nd e t e r m i n a t i o na n dc o n t i n u o u s ，h i 曲c a p a c i t y ， b i d i r e c t i o n a lt r a i n - t o - w a y s i d ed a t ac o m m u n i c a t i o i i s ，c o n t r o l l i n g t r a i n t h r o u g h t r a i n - b o r n ea n dw a y s i d ep r o c e s s o r s c b t cw a y s i d ez o n ec o n t r o l l e rp l a y sa ni m p o r t a n tr o l ei na s s u r i n gs a f l yo ft r a i n m a n a g e m e n t z cc o n t r i b u t e sr e a l - t i m ed a t at r a n s m i s s i o nw i t ho t h e rs u b s y s t e m sa n d c o n t r o l st r a i n sw i t hm o v i n ga u t h o r i t y 队) t h e r ei sg r e a tm e a n i n go fs t u d y i n gz o n e c o n t r o l l e rt r a i nm a n a g e m e n t t h ep a p e rs t a r t sw i t ht h er e s e a r c ho f z o n ec o n t r o l l e rt r a i nm a n a g e m e n t ，a c c o r d i n g t or e q u i r e m e n to fs y s t e mf u n c t i o n ，a n a l y z e ss y s t e mp r i n c i p l ei na r c h i t e c t u r e ，r e s o l l r c e a n df l o w t h ea u t h o ri n t r o d u c e sp r o c e s so fm u l t i - t r a i nm a n a g e m e n tb a s e do nt h e p u r p o s eo f m a n a g e i nt h i sp a p e r , w eu s ef o r m a lm o d e l i n gm e t h o db a s e do nh i e r a r c h a lt i m ec o l o r e dp e t r i n e t ，a n a l y s e st h ef e a s i b i l i t yo fm o d e l i n ga n dm o d e l sc p nw i t ht o pl a y e r , d a t a t r a n s m i s s i o nl a y e ra n dm ac a l c u l a t el a y e r i m p r o v ea n ds i m p l i f yt h ec p n ，t h e n s i m u l a t et h em o d e l w eu s es t a t es p a c ea n a l y z em e t h o dt ov a l i d a t er a t i o n a l i t yo fs y s t e m d e s i g na n dc o l t e c t n e s so fd a t at r a n s m i s s i o n t h i sw o r kc a nh e l pn st oc o n s t r u c tam o r e c o n s u m m a t es y s t e mm o d e lo fz o n ec o n t r o l l e r , a n dp r o v i d et h e o r yp r o o fo fz o n e c o n t r o l l e rs y s t e ms o f t w a r er e a l i z i n g k e y w o r d s ：c b t c ；z o n ec o n t r o l l e r ；t r a i nm a n a g e m e n t ；c p n ；m o d e l i n g c i 。a s s n o ：u 2 8 4 4 4 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国 家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学位论文储躲高军 导师躲 签字日期：曰年l 月必日 i 锄谤 签字日期：久呵年1 2 月2 巧日 韭塞塞通太堂亟堂僮途塞丝剑丝壁明 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作 了明确的说明并表示了谢意。 学位论文作者躲南晕签字嗍砷年棚6 日 致谢 本课题的完成，得益于许多老师和同学们的帮助，在此向他们表示衷心的感 谢。 本论文的工作是在我的导师唐涛教授的悉心指导下完成的。在两年多时间的 相处中，唐涛教授渊博的学识、严谨踏实的治学态度、实事求是的科研作风、诲 人不倦的育人精神、独到精辟的见解和科学的工作方法给我留下了深刻的印象， 使我受益匪浅，也必将使我受益终生。在此衷心感谢三年来唐老师对我的关心和 指导。 感谢实验室老师马连川、王海峰、郜春海、刘波、王悉、黄友能悉心指导我 完成了实验室的科研工作，在学习上和生活上都给予了我很大的关心和帮助。还 要感谢实验室张建民、袁磊、赵波波、徐兴华、马琳等老师对我的悉心指导，他 们对我的科研工作和论文都提出了许多的宝贵意见，在此表示衷心的感谢。 在实验室工作及撰写论文期间，刘朔、陆启劲、陈树泉、孙琳、朱镝、周家 猷、黄磊、王鹏、陈小康等同学对我论文中的研究工作给予了热情帮助，在此向 他们表达我的感激之情。同时也要向一直以来给我帮助和鼓励的杨旭文、戚番、 黄晴、孟军、张振兴、张强等师弟师妹们表示衷心的感谢。 另外也向多年来一直理解和支持我的家人表达最深切的感谢和敬意。 1 引言 1 1 选题的目的和意义 现代社会发展至今，城市轨道交通已经成为都市生活中密不可分的一部分。 在中国乃至世界上许多发展中国家，城市轨道交通的发展大都是处于发展高峰的 朝阳产业，作为一种高科技手段，它以全新的运载模式改变着我们原有的出行方 式。城市轨道交通系统作为一种安全、可靠、清洁、快捷的公共交通运输方式， 是解决我国人口密集的大城市解决日益严重的交通拥挤问题的重要手段之一。 随着无线通信技术的飞速发展，无线通信的可靠性、可用性大大提高，基于 通信的列车运行控制系统( c o m m u n i c a t i o nb a s e dt r a i nc o n t r o ls y s t e m ，c b t c ) 是 今后轨道交通列车运行控制系统的发展趋势。c b t c 系统是连续的自动列车控制系 统，它通过高精度的列车定位技术和不间断的车地通信通过提供更精确的列车 控制、持续的列车安全分隔和超速防护，使得列车可以在更短的运行间隔内实行 安全运行。 c b t c 系统是一个包含地面设备、车载设备的安全苛求系统，是大规模集成 电路、计算机、网络通信及自动化控制等多项技术在轨道交通中的综合应用。c b t c 的轨旁设备大规模集成电路、计算机的系统相当复杂，从硬件方面，即使是最简 单的计算机系统，也包含数以万计的元器件和非常复杂的行为状态；对软件来说， 比较简单的软件程序也可能有数以千计的执行路径。而复杂性对于系统安全的保 证是一个难题，复杂的系统很难设计开发，寻找错误和安全隐患也比较困难，传 统的基于黑箱测试的安全认证方法根本无法满足需要。在c b t c 系统中，轨旁设 备( 又称区域控制中心，z o n ec o n t r o l l e r ) 是整个列控系统的核心，区域控制中心 运行系统控制软件，负责列车安全间隔、列车允许速度和进路联锁等逻辑运算。 在这里，轨旁设备z c 系统以列车定位以及通信数据传输为基础的，其运算结果以 通信报文的形式通过通信子系统发送给执行单元，该子系统影响到整个c b t c 系 统的运行效率以及行车安全性，在整个系统中起到了至关重要的作用。 形式化描述方法是指在描述、设计和构建系统或软件的过程中所使用的基于 形式逻辑和离散数学的方法和技术。它用严格的数学符号和数学方法对目标系统 的结构与行为进行有效的综合、分析和推理，它为系统的说明、开发和验证提供 了一个框架，利于发现目标系统需求中的不一致性、不完整性等方面。形式化方 法已经可以适用于一定规模和复杂性的系统开发，支持软件开发的多种活动如需 求描述、设计、验证、正确性证明和测试等。 轨旁设备区域控制中心系统运行管理系统的体系结构是否合理，直接关系到 区域控制中心系统能否稳定运行，甚至关系到c b t c 控制系统能否正常进行。因 此，对轨旁设备z c 系统的设计与开发进行研究具有重要的意义。而对于c b t c 系 统的软件开发。有必要采用一种形式化方法来精确规范系统功能结构，并对系统 的形式化特性进行研究。本论文的研究对象为轨旁z c 对内部各列车在移动闭塞条 件下运行的管理过程。采用形式化的基于层次时间有色p c t r i 网的建模方法对上述 过程进行模型的构建，用有色p e 仃i 网分析的软件支持工具c p nt o o l s 实现对模 型的自动化仿真并采用p e t r i 网方法所独有的多种分析技术，对模型的各种特征， 如可达性、死锁等进行分析，验证系统设计各方面的合理性、完备性与安全性。 为进行轨旁z c 系统的软件设计与软件分析提供了依据，更好的服务于c b t c 系统 z c 子系统的软件开发。 1 2c b t c 系统综述 1 2 1 基于通信的列车控制系统( c b t c ) 简介 为满足经济增长的需求，许多国家都在大力发展高速铁路。在我国，铁路运 输是国民经济的大动脉，铁路的运能必须适应国民经济不断增长的对铁路运量的 需求。为此，在大力建设新线路的同时，我国铁路部门一直致力于增加列车重量、 提高列车的行车速度和增大行车密度，提高既有线路的列车通过能力。我国铁路 部门已先后6 次大规模列车提速，提速总里程近1 万公里，覆盖了全国铁路主要 线路。 我国现有铁路控制系统主要为基于轨道电路的列车控制系统( t b t c - t r a c k c i r c u i t b a s e d t r a i n c o n t r 0 1 ) 。该方式为保障行车安全，提高行车效率发挥了巨大作 用，但由于t b t c 利用轨道电路传输地面至车上的信息、检测固定闭塞分区的占 用情况，它存在信息量不足、轨道电路工作稳定性易受环境影响、线路通过能力 易受损、维护费用大等。 为改善轨道电路存在的上述弊端，提出了大量新型的控制理念和方法，如在 列车与地面之间增加信道来实现列车到地面方向的通信。2 0 世纪6 0 年代，我国著 名专家汪希时教授提出了“移动自动闭塞系统”，并指出使用无线方式实现车地间 双向通信。到8 0 年代，借力于数字通信技术、无线通信技术、编码技术的迅速发 展，发达国家相继出现使用无线车地通信的应用方案，如：美国的先进列车控制 系统( a d v a n c e dt r a i nc o n t r o ls y s t e m ，a t c s ) 、欧洲列车控制系统( e u r o p e a nt r a i n 2 c o n t r o ls y s t e m ，e t c s ) 等等。这种列车运行控制系统被称为基于通信的列车控制 ( c o m m u n i c a t i o n s b a s e dt r a i nc o n t r o l ，c b t c ) 系统【2 】。 c b t c 系统是连续的自动列车控制系统，使用高精度列车定位，不再依赖轨道 电路；使用连续、大容量的车地双向数据通信；车载设备和轨旁设备实现安全功 能。 城市轨道交通c b t c 系统的主要构成部分有：中央控制设备、中央数据库、 轨旁控制器、车载控制器、数据通信网络以及相关轨旁设备( 如道岔、信号机等) ， c b t c 系统框图如图1 1 所示【3 】。 尚尚尚 【应答器j j _ j 图1 1c b t c 系统框图 f i g 1 1c b t cs y s t e md i a g r a m 查询应答器用于列车定位。应答器一般安装在轨枕上面。当列车通过应答器 时，车载设备读取应答器中的相应信息，并使用该信息作为索引，在车载控制器 数据库中查找相关信息。同时列车始终通过测距设备得到至最近通过的应答器的 行驶距离，从而可在任意时刻获得准确的列车位置。 列车在行驶过程中，按照一定周期将自身位置和行驶速度等行车状态信息通 过无线通信发送给当前位置所属的轨旁控制器。 轨旁控制器结合中央控制设备发出的行车指令、列车状态和前行列车状态， 通过通信网络向列车发送控制命令，同时控制轨旁设备进行相应动作，确保列车 3 安全、高效的运行。 中央控制设备通过网络获得整个系统内各个设备的状态，包括列车行驶状态、 列车当前位置、道岔状态等信息。同时，中央控制设备可以向轨旁控制器发出控 制命令，执行单独安排进路、单独操作道岔和设置临时限速等操作。 由此可见，c b t c 系统的基本特点在于：( 1 ) 不再依赖轨道电路的准确列车定 位；( 2 ) 通过连续的车地、地车通信网络，大大增加了控制信息和车辆状态信息的 信息量；( 3 ) 地面设备和车载设备协同工作，提供强大可靠的列车安全防护。 1 2 2 基于通信的列车控制系统( c b t c ) 的发展概况 1 9 9 9 年9 月，i e e e 制定了第一个c b t c 标准，( i e e es t d1 4 7 4 1 1 9 9 9 ) ，将 c b t c 定义为：利用( 不依赖于轨道电路的) 高精度列车定位、双向大容量车地 数据通信和车载、地面的安全功能处理器实现的一种连续自动列车控制系统。 自8 0 年代初北美推出a t c s 以来，受到一些经济发达国家的普遍重视，欧洲、 日本等国相继探索和研制类似的系统，如北美的a r e s ，欧洲的e t c s 、法国的 a s t r e e ，德国的f z b 、日本的c a r a t ，形成了世界性趋势。9 0 年代前后，这些 系统分别在各国铁路列车控制领域中逐步得到实施，有的已投入应用，显示出其 巨大的优越性和强大的生命力。目前，c b t c 技术已凭借自身优点成为新一代列控 的发展方向。发达国家对于高速铁路基于通信的列控系统的研究已形成欧洲、美 国、日本3 大体系【4 】。 1 美国a a t c 美国于1 9 9 2 年初提出了基于无线通信的“先进的自动化控制系统( a a t c ) ”。 a a t c 属于c b t c 系统，最突出的特点是列车定位使用扩频通信方式，采用军用 加强型定位报告系统，沿线安装无线电台，路旁无线电台将测定信号送至控制中 心，控制中心根据无线电波传播时间计算出列车所在位置，并根据列车定位计算 出列车安全运行速度，车站由此可解决列车定车距离、发送安全行车速度码以及 加速命令，实现对列车的控制。 2 日本a t a c s 为了迎合c b t c 系统在全世界铁路的发展，日本于1 9 9 5 年由日立公司开发研 制了一种基于双向无线通信的先进列车管理与通信系统( 朋r a c s ) 。该系统的列车 控制也不再基于轨道电路，而采用了c b t c 技术。在a t a c s 中，将铁路线路划分 成若干个控制区，每个控制区有一个地面控制器和一个无线电基站。地面控制器 完成一些控制功能，它与相应的无线电基站相联。地面控制器接收列车坐标信息 后，就能进行列车运行的间隔控制。在编组站还有进路控制在平交道口则对道 4 口信号及栏杆进行控制。无线电基站则通过移动无线电方式将列车位置参数、运 行速度等数据传送至车载设备，以此完成车载设备与地面之间的信息交换。 3 欧洲e t c s 1 9 9 1 年，欧共体国家签署了研制“欧洲列车控制系统e t c s ”的备忘录，由 欧共体资助e t c s 的研究和试制工作。1 9 9 2 年1 月，国际铁盟( u i c ) 给出e t c s 的 项且说明、相关的功能和系统的技术规范。详细的规范( 包括e t c s 的功能条件、 系统技术条件、各相关子系统的技术条件以及有关系统安全、环境、可靠性等的 技术条件1 由欧洲铁路研究所( e r r i ) 的a 2 0 0 小组于1 9 9 6 年6 月完成。e t c s 在实 施方面划分为5 个应用等级：e r t m s e 1 s 等级0 、e r t m s e t c s 等级s t m 、 e r t m s e t c s 等级l 、e r t m s e t c s 等级2 、e r t m s ，e t c s 等级3 ，高等级向下 兼容，各国可根据本国实际情况采用相应的等级的e t c s 系统。其中，e r t m s e t c s 等级2 和e r t m s e t c s 等级3 采用g s m r ( g s m ? f o rr a i l w a y s ) 技术来实现地 面与列车之间双向的信息传输，因此这两个等级属于c b t c 范畴。e t c s 实现了欧 洲各国铁路的互操作性。 c b t c 系统已在全世界范围发展，我国铁路及有关单位对c b t c 技术的开发 也一直在努力进行，自1 9 9 3 年起北京交通大学就开始启动了c b t c 技术的开发立 项。 目前，我国铁路列车控制系统主要采用传统的基于轨道电路的列车控制方式 ( t b t c ) ，只能完成以简单控制信息为主，速率仅几十b i t s 的地、车单向数据传 输，这种智能化程度低的状况已经不能适应现代铁路运输发展的需要。为了实现 铁路的战略化发展，我国铁路部门和科研机构在积极学习国外先进技术和经验的 基础上，研究适合我国铁路特殊要求的c b t c 系统。 l 。3c b t c 系统列车运行管理概述 1 3 1c b t c 系统管理列车运行的闭塞方式 c b t c 系统可实现移动闭塞方式( m o v i n g a u t o m a t i c - b l o c ks y s t e m ，简称m a s ) ， 它摆脱了轨道电路，也不需要将轨道分成若干分区，并为每个分区分配状态。采 用c b t c 系统，每列列车都能够精确测定自身在轨道上的位置，并将这些信息发 送给轨道旁的区域控制系统，c b t c 系统利用此信息为每列列车分析、计算安全运 行参数，包括安全行驶路线、安全运行速度已经目标停车点。目标停车点将根据 前方列车的移动、轨道状态、当前列车速度精确计算移动的停车点。 当列车车载设备发生故障或列车前方出现障碍物时，列车和旅客能够置身于 5 一个受到保护的区域内，即列车紧急制动后，在这个区域内能够安全地停车，一 定不会与任何阻碍物( 包括其他列车) 相撞，也不会由于道岔位置没有调整到位 而发生脱轨事故。这个安全区间会随着列车的移动而移动，故称移动闭塞【5 1 。它与 固定闭塞相比，最显著的特点是取消了以信号机分隔的固定闭塞区间。列车间的 最小运行间隔距离由列车在线路上的实际运行位置和运行状态确定，所以闭塞区 间随着列车的行驶，不断地向前移动和调整。在移动闭塞技术中，闭塞区间仅仅 是保证列车安全运行的逻辑间隔，与实际线路并无物理上的对应关系。因此，移 动闭塞在设计和实现上与固定闭塞有比较大的区别。其中列车定位( t r a i n p o s i t i o n ) ，安全距离( s a f e t yd i s t a n c e ) 和目标点( t a r g e tp o i n t ) 是移动闭塞技术 中最重要的3 个基本要素 6 】口 移动闭塞系统摆脱了用轨道电路判别列车对闭塞分区占用与否，突破了固定 或准移动闭塞的局限性，具有更大的优越性和特点，主要表现在以下方面： 1 1 实现列车与轨旁设备实时双向通信，且信息量大。 2 ) 可减少轨旁设备，便于安装维修，有利于紧急状态下利用线路作为人员疏 散的通道，有利于降低系统全寿命周期内的运营成本。 3 ) 便于缩短列车编组，进行高密度运行；可以降低土建工程投资；有利于实 现线路列车双向运行而不增加地面设备。 4 ) 可适应各种类型、各种车速的列车，由于移动闭塞系统基本克服了准移动 闭塞和固定闭塞系统地对车传输信息发生跳变的缺点，从而提高了列车运 行的平稳性，增加了乘客的舒适度。 5 ) 可以实现节能控制、优化列车运行的统计处理、缩短运行时分等多目标控 制。 6 ) 移动闭塞系统，尤其是采用高速数据传输方式的系统，将带来信息利用的 增值和功能的扩展，有利于现代化水平的提高。 7 ) 由于移动闭塞系统具有很高的实时性和响应性的要求，其对系统的完整性 要求高于其它制式的闭塞方式，系统的可靠性也有了更高要求【7 1 。 1 3 2 移动授权( m a ) 的概念和作用 在城市轨道交通中，c b t c 系统的主要任务是保证列车在系统控制的线路内安 全运行。这是通过为每列通信列车提供一个移动授权( m o v e m e n t a u t h o r i t y ，m a ) 来完成的。 m a 的具体定义是指从列车的车尾起到前方终点障碍物的这部分线路。当列车 在受控线路区域内按照正常时刻表运行时，v o b c 将列车的位置与运行方向发送 6 给z c ，并根据自己的制动曲线来决定是否向z c 申请m a 的延伸，而z c 使用列 车当前位置、行驶方向、进路以及周围线路的当前状态( 来自于c i ) 来确定每列 列车的m a ，然后通过d c s 通信子系统向v o b c 传达列车的m a 。整个过程中， z c 实时地与d s u 、v o b c 、c i 等子系统进行信息交互，有规律地、周期性地通过 d c s 系统向其管辖区域内运行列车的v o b c 发送m a ，同时z c 还会把列车m a 内的进路及障碍物状态告诉v o b c 。m a 的含义可以用图1 2 表示。 图1 2 m a 的含义 f i g 1 2d e f i n i t i o no f m a m a 是由z c 子系统生成的，因此z c 是m a 的制造者。在生成m a 的过程中， z c 将会处理到很多种类的障碍物，从中选取符合条件的能够作为列车此周期运行 终点的终点障碍物。终点障碍物既有可能是静态障碍物，例如道岔，进路终点等； 又有可能是动态障碍物，例如前方列车的m a 等。 列车的m a 会有规律地、周期性地重建。m a 结构是从列车当前位置开始并 且从列车行驶方向延伸至最近的障碍物。探测到系统状态( 如前面列车的运动、 占用、线路关闭区域、道岔动作) 的改变后，z c 将重新计算，并将调整后的m a 发给列车，而列车又不断地将新的位置发给z c ，该位置在列车重建m a 过程中将 被使用，并且对其它列车来说是个障碍物。 z c 管理列车并为其提供m a ，因此列车是m a 的使用者。 在v o b c 子系统中，车载控制设备实时比较列车的实际速度与接收到的m a ， 当列车实际速度超过m a 的限制速度，将自动实施常用制动或紧急制动，保证列 车安全停在安全点前。 z c 管理列车并进行m a 计算涉及到c b t c 系统中多个子系统之间的信息交 互，m a 是联系各子系统的纽带，并且直接影响线路的通行效率和c b t c 系统的 安全运行。 7 1 4 形式化的描述与验证技术 1 4 1形式化方法的定义与分类 形式化描述方法是指在描述、设计和构建系统或软件的过程中所使用的基于 形式逻辑和离散数学的方法和技术。它用严格的数学符号和数学方法对目标系统 的结构与行为进行有效的综合、分析和推理，它为系统的说明、开发和验证提供 了一个框架，利于发现目标系统需求中的不一致性、不完整性等方面。它具备以 下重要的特性： 数学模型； 它是否可以表达“做什么”，而不需要说“怎样做”； 形式化的语法； 它是否可以方便的应用有效的工具来进行自动化分析【s 】。 根据对目标系统进行说明的方式，形式化方法可以分为如下两种： 1 面向模型的方法。在面向模型的方法中，对目标系统的说明是为其构造一 个模型，该模型的构成成分是一些具有特性的数据抽象，如域、元组、集 合、序列、包、映射等。 2 面向性质的方法。这种方法通过直接给出目标系统的，一组特性来描述目 标系统，通常是一组目标系统必须满足的形式公理。在面向性质的方法中， 其形式规格说明仅描述目标系统的性质，而不涉及实现方法。 根据表达能力，形式化方法大致可分为五类： 1 基于模型的方法。给出系统( 程序) 状态和状态变换与操作的显式但亦是 抽象的定义，但对于并发没有显式的表示，如基于模型的形式规约语言z 和v d m 。 2 代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而不 定义状态，同样它亦未给出并发的显式的表示，如基于性质的代数规约语 言o b j 、l a r c h 、c l e a r 。 3 过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可观 察的通讯上的限制( 约束) 来表示行为，如c s p 、c c p 。 4 基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序允许 的低级规范和系统时间行为的规范，如时态逻辑。 5 基于网络的方法。根据网络中数据流显式地给出系统的并发模型，包括数 据在网中从一个结点流向另一个结点的条件。如p e m 网、谓词变换网。 对形式化描述化方法的分类是很难的，有的形式化描述方法可能同时属于多 8 个类别，这主要依赖于该形式化描述方法在实际工程中如何运用。但总的来说， 上述划分有助于比较各形式化描述方法的异同。 没有哪一种形式化描述方法适合描述和分析复杂系统的所有方面。大多数形 式化描述方法都是基于单一的形式化描述语言的，它们只适合描述系统的某些方 面，如控制流、数据、结构、行为等等；或只适合描述某种类型的系统，如顺序、 并发、分布、实时等等。在实际应用中，往往需要使用多种形式化描述方法对系 统的不同侧面进行描述和分析。 1 4 2p c t r i 网与嵌入式系统建模 在高层规范至最终实现的过程中，选用适当的、以形式化方法为基础的工具 进行辅助设计和验证，是提高产品质量的主要途径。p c t r i 网建模方法是形式化建 模方法的一种。p e 缸网是一种系统的数学和图形的描述和分析工具。对于具有并 发、异步、分布、并行、不确定性或随机性的信息处理系统，都可以利用这种工 具构造开发p c 嫩- i 网模型，然后对其进行分析，即可得到有关系统结构和动态行为 方面的信息，根据这些信息就可以对要开发的系统进行评价和改进。p c t r i 网以其 模型的直观图形表示和方便的模型分析能力在线路设计、网络协议、软件工程、 人工智能、形式语义、操作系统、并行编译、数据管理等计算机学科的诸多领域 获得了广泛应用。 经过几十年的发展，p e t d 网理论已逐步成熟，成为一种非常有用的模型工具。 p e t r i 网研究的系统模型行为特性包括：状态的可达性、位置的有界性、变迁的活性、 初始状态的可逆达、标识之间的可达性、事件之间的同步距离和公平性等。p c t d 网模型的主要分析方法依赖于：可达树、关联矩阵和状态方程、不变量和分析化 简规则、结构理论等。p c t r i 网本身也经历了从简单到复杂的过程，其抽象描述能 力也在得到不断的丰富。p c t r i 网的抽象描述能力在不断的得到丰富：从基本的条 件时间网( c e ) ，位置变迁两j ( p t ) ，谓词变迁网到有色网( c p ) ：从没有时间的p c t r i 网到时间p e t r i 网；从一般有向弧发展到禁止弧，从自然数标记个数到概率标记个 数：从原子变迁到谓词变迁和子网变迁等等。 1 9 9 2 年，p c t r i 网被首次提出作为嵌入式系统建模方法，它可以很好的处理同 步并在编码前检测出一些问题。但是，p c t r i 网模型也存在一个问题：状态空间随 着状态元素的增加呈指数增长，所以它只能运用于比较小的系统，对于大系统建 模显得不必要。此外，这样的p e t r i 网模型是一种与系统高度相关的模型，缺乏模 块性、可重用性、可维护性。因此，一种用于嵌入式系统设计的面向对象的p c t r i 网被提出，在嵌入式系统应用中获得了很大的成功。 9 1 4 3 有色p e t r i 网理论与c p nt o o l s p e t r i 网具有形式化语义、图形化本质的特征，直观易于学习，表达能力强， 同时可以选择大量的分析方法，在系统的早期设计阶段可以发挥强大的作用。但 当所要研究的系统极为复杂时，采用基本p e t r i 网模型，常会导致过多的位置节点 和变迁节点，从而使运用p e t r i 网进行分析验证的复杂性大为增加。此时，通过对 p e t r i 网进行某些扩展，是减少基本p e t r i 网模型结构复杂度的有效途径。其中，有 色p e t r in ( c o l o r e dp e t r in e t s ，c p n ) 是一种在p e t r i 网基础发展起来的适用于描述 并行和异构网络的系统分析和设计工具，其最大的优点就是具有直观性及严谨的 数学理论基础。 c p n 的特点是把系统中具有类同行为的元素归属到一个库所节点或一个变迁 节点中，并通过对所属标识颜色的不同来进行区别，从而使p e t r i 网的结构得到很 大程度的简化。 相比于基本p e t r i 网，有色p e t r i 网具有两个不同之处： 1 对不同属性的标识着以不同的颜色，并把着了颜色的标识称为有色标识或 色点。在c p n 中，一种颜色的“有色标识”用来表征一类具有相同行为 特性的元素。而在基本形式p e t r i 网中，一个“标识”仅仅只是表示一个 元素或一个资源； 2 c p n 标识的激发不同于基本p e l r i 网的激发规则。在c p n 中，任意两个节 点间的路径弧上，都标示一个相应的线性函数。每个线性函数明确地规定 了相应的激发条件，包括为使变迁节点使能，其输入位置节点中所应有的 色点的颜色，以及变迁节点在完成发射后应清除的和应产生的色点的颜 色。 通过把更多的系统结构信息压缩于一个节点中，使得采用c p n 来描述系统时， 比基本p e t r i 网要简洁得多。特别是描述复杂的大规模系统时，有色p e t r i 网更能显 示出巨大的优越性。 支持c p n 的计算机建模工具也很多，其中c p n t o o l s 是有色p e t r i 网领域中著 名的计算机仿真软件。c p nt o o l s 是丹麦的奥胡根大学( t h eu n i v e r s i t yo f a a r h u s ) 和美国宇航局于2 0 0 0 年4 月联合推出的基于c p n 的仿真软件。长期以来，p e t r i 网作为一种有效的离散事件建模工具，建立了许多的仿真模型，但是由于缺少一 种可靠易用的仿真平台对其有效的支撑，使得其仿真模型仅限于理论研究的层面， c p nt o o l s 的出现改变了这一局面。该工具能够提供与环境相关的信息反馈，指出 网元素之间的依赖关系。在网的构建过程中，工具能够进行语法检查以及代码生 成，快速仿真模拟器能够有效处理非时间和时间关联的有色p e t r i 网，此外还能够 1 0 自动地生成并分析完全的和部分的状态空间，并且，生成的标准状态空间报告包 含诸如有界性、活属性等动态属性信息。现已广泛应用于政府、科研单位。 c p nt o o l s 能够完成有色p e t r i 网的编辑、语义检查、网络模拟、状态空间分 析等功能。在c p nt o o l s 中编辑有色p e t r i 网，经常有多种方式来执行同一特殊任 务，因而显容易、快捷并且灵活。当编辑c p n 时，c p nt o o l s 以多种方式协助用 户，诸如，提供许多关于网的语法和工具状态的图形反馈，自动对准绘制各个项 目对象。菜单中的工具能够应用于单个变迁或者是某个页，如果相关的页包含多 个使能变迁，则从中随机选择一个变迁进行实施。c p nt o o l s 工具仿真运行机理在 于基于网结构和文本表达式将网编译成m l 代码，使得在编辑时能够对网进行不 断的校验。校验和仿真可能会导致语法和运行时错误，这会被明显显示出来。对 于分层c p n ，如果错误不是出现在项层页中，则有错误的任何页的标签上会出现 明显的错误标示。 1 5 论文的研究内容 本课题研究的是在c b t c 系统中起到核心地位的区域控制中心系统对于内部 列车运行情况的管理过程，并用一种形式化的方法一有色p c t r i 网理论对完成列 车管理模型的构造。研究结合自主研发的c b t c 系统，通过分析z c 列车运行管理 的原理提供建模思路，采用层次时间有色p e t r i 网来对列车管理整个过程进行建模， 并用有色p c t r i 网的分析方法完成了模型性质的分析。这对于完成c b t c 区域控制 中心的全面开发和设计有着十分重要的意义，为进行轨旁z c 系统的软件设计与软 件分析提供了依据，更好的服务于c b t c 系统z c 子系统的软件开发。 论文的结构如下： 第一章引言。论述了选题的目的和意义，简要介绍了c b t c 系统及其在国内 外的发展状况，大体介绍了c b t c 系统管理列车运行的概念与手段，并介绍复杂 系统的形式化分析验证方法，最后介绍了本文的结构。 第二章区域控制中心列车运行管理的原理。根据区域控制中心系统的需求详 细分析了z c 列车运行管理的原理，包括管辖区域列车的各种运行状态和多车追踪 运行的情况，最后介绍了z c 列车管理过程的具体实现。 第三章区域控制系统列车管理的建模。引入了层次时间有色p e t r i 网这一复杂 系统建模的概念，分析了采用这种建模方法对列车管理情况建模的可行性，分层 设计管理流程，完成了区域控制中心列车管理模型的构建。 第四章列车管理模型的仿真及分析。在第三章构建的系统基础上，通过在 c p nt o o l s 中设置初始化标识对所建立模型进行仿真，模拟列车管理全过程。并利 用仿真工具采用的状态空间分析技术对模型性质进行验证。 第五章结论与展望。 1 6 本章小结 1 1 阐明了选题的目的和意义； 2 ) 介绍了基于通信的列车控制系统( c b t c ) 的原理以及发展技术概况； 3 1 介绍了c b t c 系统列车运行管理的闭塞方式和相关概念； 4 1 介绍了系统的形式化描述与验证技术； 5 1 介绍了本文的主要研究内容。 2 区域控制中, b n 车运行管理的原理 区域控制中心( 轨旁设备z c ) 在保证列车安全运行方面发挥着重要作用，它 负责实现列车安全间隔运行等功能，对区域内部运行的列车进行管理。区域控制 中心是基于通信的列车运行控制系统中保证行车安全的关键设备，对于系统软硬 件的实时性、安全可靠性要求很高。 作为本文重点研究的对象，区域控制中心系统将各个子系统串联起来，成为 整个c b t c 系统正常运作的纽带。系统对列车的管理，就是在移动闭塞的条件下 管理控制列车的安全运行。在对整个列车管理过程进行建模之前，有必要对移动 闭塞下列车管理的原理进行深入的分析，从根本上弄清楚移动闭塞的基本原理， 在列车运行管理的过程中，生成者区域控制中心需要完成哪些功能，以及使用者 列车将会经历哪些状态的转换，整个过程中将表现为何种资源形式的转移，这些 都是使用有色p e t r i 网进行建模分析所关心的。同时列车运行管理的具体实现也直 接影响到建模分析的成败。 2 1 移动闭塞的基本原理 移动闭塞是基于区间闭塞原理发展起来的一种新型闭塞技术。它与固定闭塞 相比，最显著的特点是取消了以信号机分隔的固定闭塞区间。列车间的最小运行 间隔距离由列车在线路上的实际运行位置和运行状态确定，所以闭塞区间随着列 车的行驶，不断地向前移动和调整，称为移动闭塞。 在移动闭塞技术中，闭塞区间仅仅是保证列车安全运行的逻辑间隔，与实际 线路并无物理上的对应关系。因此，移动闭塞在设计和实现上与固定闭塞有比较 大的区别。其中列车定位( t r a i n p o s i t i o n ) 、安全距离( s a f e t y d i s t a n c e ) 和目标点 ( t a r g e tp o i n t ) 是移动闭塞技术中最重要的3 个概念 6 3 。 1 列车定位 列车定位是移动闭塞技术的基础。要实现闭塞区间的动态移动，首先必须实 时、准确地掌握列车的位置信息，确定列车间的相对距离。系统不断地将该距离 与所要求的运行间隔距离相比较，确定列车的安全运行速度。所以说，没有准确 的列车定位，就没有移动闭塞。 列车定位由地面设备和车载设备共同完成。通常在列车的轮轴上安装有车轮 转速计，确定列车的走行方向和距离。一旦列车运行的起始点确定以后，根据车 轮转速计所检测到的列车运行方向和走行距离，就可以精确地确定列车在线路上 些塞銮适盍堂亟堂僮途塞匡燮撞剑生! 坠到主运短萱堡鳆厘垄 的实际位置。 但是，由于车载定位设备存在着测量误差，特别是列车经过长距离运行后， 这个误差会不断地积累，直接影响列车定位的精度，所以，在线路上每隔一定距 离，就需要安装1 个地面定位设备。当列车经过这些地面定位设备时，由车载传 感设备检测到该定位点，获知列车的确切位置，从而消除车载定位设备所产生的 累积定位误差。 2 安全距离 安全距离是基于列车安全制动模型计算得到的1 个附加距离。它保证追踪列 车在最不利条件下能够安全地停止在前行列车的后方，不发生冲撞，所以，安全 距离是移动闭塞系统中的关键，是整个系统设计的理论基础和安全依据。以下结 合图2 1 讨论安全距离的基本概念。 停车点不确定位置 一常用制动距离+ 一安全距离 图2 1 安全距离示意图 f i g 2 1s a t e t yd i s t a n c es c h e m a t i cd i a g r a m 如图2 1 所示，假定追踪列车以线路允许的最高速