摘  要 传统的软件开发方法不能满足基于通信的列车控制( CBTC) 区域控制系统( ZC) 的开发需求。结合北京地铁亦庄线研究项目，介绍一种基于模型的系统开发方法，给出 ZC 系统的软件容错结构，阐述该系统的移动授权和列车管理功能建模方法，并从模型覆盖率分析和形式化验证两方面深入分析系统安全性保障措施。ZC 系统的研究项目表明，基于模型的开发方法能够更好地保证系统的开发质量和安全性。

关键词 城市轨道交通 基于通信的列车控制 区域控制 基于模型开发 安全苛求 北京地铁亦庄线

 

      近年来，随着轨道交通的蓬勃发展，为确保列车运行安全和提高运输效率，基于通信的列车运行控制( communication based train control，CBTC) 系统^［1］已成为发展方向。CBTC 系统通过高精度的列车定位和连续的车地通信技术，提供更精确的列车安全间隔控制和速度防护，最大限度地提高列车运行效率。CBTC 是典型的具有 SIL4 等级要求的高安全系统，伴随着功能的不断增强，系统对软件的依赖性越来越强。在传统的软件开发方法中，系统的设计过程多利用自然语言表达，易引起理解上的歧义，对系统设计的分析验证更多地依赖于人工方式，很难保证设计的正确性，对系统功能的测试需要在开发周期的后期进行，一旦发现错误，修正的成本极其昂贵。所以，传统软件开发方法已不能很好地应对 CBTC 开发所面临的挑战。

      基于模型系统开发( model-based development，MBD)方法的出现^［2-4］，引起了安全关键领域系统开发方式的变革。这种方法基于严格的数学理论，使系统描述模型化，在模型的基础上进行设计、分析和验证，最终基于模型来实现系统。目前，在安全苛求领域，基于模型的开 发 方 法 发 展 比 较 迅 速，出 现 了 诸 如 Matlab-Simulink / Stateflow、UML、SCADE 的开发工具^［4-7］。20 世纪 80 年代，SCADE 在 Lustre 同步模型语言的基础上被开发用来进行航空系统的设计，90 年代推广应用到安全关键软件开发领域，它具有面向模型的图形用户接口、动态仿真和系统状态分析的功能，并且支持连续或离散时间的线性和非线性系统。

      下面结合北京地铁亦庄线 CBTC 系统的研究项目，以区域控制( zone controller，ZC) 系统为例，介绍基于 SCADE 模型的 CBTC 系统安全苛求软件开发方法。

 

      ZC 系统是 CBTC 系统中的地面列车自动防护子系统，负责所辖区域内所有列车运行的安全。ZC 系统是安全完整性等级要求最高的子系统之一，对系统安全软件的设计开发要求极为苛刻。

      亦庄线是连接北京市中心城和亦庄新城的轨道交通线路，如图 1 所示。全线设置 6 座设备集中站、6 个ZC 系统，初期配置 23 组列车的车载设备，是国产CBTC 系统的首次运用。亦庄线起点位于宋庄路与石榴庄路交叉口南侧，全线共设车站 14 座，其中地下车站6 座、高架车站 8 座。全线换乘车站共 5 座在宋家庄站与 M5、M10 换乘，在旧宫站及荣京东街站与 L5 换乘，在经海路站与 M12 换乘，在亦庄火车站与京津城际及 S6换乘。控制中心设在小营，备用控制中心设在车辆段信号楼内。全线设置宋家庄停车场和亦庄车辆段。

      ZC 系统运行于 2 取 2 乘 2 安全计算机平台，通过以太网与其他部分进行信息交互，从总体上划分为列车状 态 信 息 管 理、设 置 与 处 理 移 动 授 权 ( moving athority，MA) 、强制命令与辅助功能、数据库版本比较、故障处理以及为系统提供维护诊断信息等几大功能模块。ZC 系统对管辖范围内的列车进行管理，根据列车位置信息，计算生成移动授权，并辅助联锁等设备完成列车的定位和室外设备的控制，并周期性地与车载设备( VOBC) 、联锁设备( CI) 、列车自动监控设备( ATS) 、数据存储单元( DSU) 系统进行信息交互，监控通信情况，实时更新管辖范围内的设备运行等信息，并作为控制列车运行的因素。

      在系统开发中，ZC 系统采用了 2 取 2 双版本安全软件容错结构，如图 2 所示。ZC 系统的双版本代码基于同一个详细设计，采用两种不同的方式进行开发，一种为传统的手工编写代码的开发方式，另一种为基于SCADE 模型开发的方式，通过比较双版本软件的运行结果来输出最终结果。

      基于 SCADE 对 ZC 系统进行建模，主要分为数据流图和安全状态机。两套机制都建立在严格的数学模型基础之上，具有严格的数学语义，能够保证设计模型的精确性、完整性、一致性和无二义性。作为 ZC 系统的核心功能，移动授权计算以及列车管理在控车过程中发挥了关键作用，ZC 系统其他功能模块的实现都会依托于这两个功能模块。考虑移动授权计算着重于逻辑处理，选择数据流图予以实现; 而列车管理主要涉及状态跳转，选择安全状态机予以实现。

      移动授权是指车载 VOBC 按照给定的运行方向被授权进入和通过一个特定的轨道区段( 见图 3) ，它在每个通信周期前动态计算生成。系统执行移动授权，以维持安全的列车间隔，并通过联锁提供防护。

      移动授权在每个周期内更新，全部为安全信息，其组成可以划分为 ZC 发送给车载 VOBC 的移动授权限制、移动授权范围内包含的所有轨旁设备状态、由于运营需要设置的临时限速等影响列车行车安全的信息。在生成移动授权的过程中，ZC 系统会处理很多种类的障碍物，从中选取符合条件的、能够作为列车此周期运行终点的障碍物。终点障碍物既有可能是静态障碍物，如道岔、进路终点等，又有可能是动态障碍物，如前方列车等。列车的移动授权会有规律、周期性地重建。

      按照 MA 计算步骤，将模型划分为 MA 初始化节点、遍历通信车节点、遍历非通信车节点等部分，通过各部分相互间的数据流向组成 MA 计算整体模型( 见图 4) 。MA 初始化结果作为是否继续计算 MA 的判断依据，遍历通信车节点判断所处理列车前方是否包含通信列车，遍历非通信节点判断所处理列车前方是否包含非通信列车。

      区域控制器处理的主要对象是在区域控制器管辖范围内的列车。根据列车在 ZC 范围内的不同行为，可以将列车划分为不同状态; 按照不同状态，ZC 将会对列车进行不同处理，以满足列车当前状态的需求。

      不同状态的列车之间存在相互转换的关系( 见图 5) 。当列车在 ZC 管辖范围内满足一定条件时，可以从一个状态转换至另一个状态; ZC 通过对列车实施状态跳转控制，完成对管辖范围内列车的管理工作。

      基于 SCADE 软件，采用状态机建模( 见图 6) 方式，实现列车管理功能。首先定义模型层次，将所有列车状态抽象划分为正常状态与故障状态。正常状态包含列车正常行驶过程中可能经历的全部状态，其中初始状态被设置为状态机模型的起始端。处于正常状态中的各个列车状态通过一系列的变迁约束条件相互关联，一旦条件满足，则状态转换会被马上触发。当 ZC判断出列车发生故障时，状态机内层将会终止，正常状态直接转换至故障状态。

      在建立数据流图与安全状态机的模型后，可以将两套模型的开发机制融合在一起，将数据流图模型的嵌套在状态机中，以实现混合系统的开发。

 

      在完成模型建立工作后，需从安全角度对所建立的模型进行测试及验证，以保证基于模型开发的 ZC 系统的安全性及可靠性。SCADE 软件提供模型覆盖率功能和形式验证功能来完成对所建立模型的验证，前者能够对模型的完备程度进行定量评估，后者则基于严格的数学推理过程，是被广泛认可的验证方式。

      利用模型覆盖率的分析功能，可以根据预定义或自定义的覆盖率准则，分析仿真场景在模型中的覆盖程度，并能指明未覆盖的路径。当覆盖率未达到要求时，很有可能会暴露开发过程中的诸多问题，如需求错误、模型设计错误等。

      针对 ZC 系统的不同功能模块，设计了一系列的仿真场景，通过基于模型的覆盖率分析，直观地展现测试的效果( 见图7) 。通过不同颜色的显示，可以直观地看出哪些模块单元部件已经充分测试，哪些还没有被彻底测试。在分析过程中，发现问题并解决问题，直至系统达到完备。

      模拟仿真和模型覆盖率分析能够在一定程度上测试系统模型是否实现所期望的功能，但并不能保证系统满足所有的安全性要求。

      借助于形式验证功能，可以借助形式验证工具，对ZC 系统进行自动化的验证过程( 见图 8) 。由于是基于严格的数学推理过程，因而保证了该验证过程是详尽、可信的。形式验证不需要借助测试用例，只需模型在描述安全性要求和建立一个“特性观察器”之后，即可自动验证模型的安全性。如果模型是安全的，它能给出一个安全的证明; 如果模型是不安全的，它能给出一个反例来帮助纠错。可见，形式验证在很大程度上保证了目标系统的安全性。对于 ZC 系统中的核心功能( 如 MA 计算) ，采用形式验证能够有效地保障系统安全。

      笔者结合北京地铁亦庄线的科研项目，介绍了一种基于模型的 CBTC 区域控制 ZC 系统的安全关键软件开发方法，给出了系统的容错结构，阐述了 ZC 系统的建模方法和安全性保障措施。亦庄线已于 2010 年12 月 30 日正式开通运营，系统安全、稳定。结果表明，基于模型系统开发具有如下优点: 一是利用严格的形式化模型手段描述系统的功能，可使系统设计更为精确; 二是模型能够充分地刻画系统的行为，能够更加完备地分析验证系统的设计; 三是给设计人员提供了在系统开发早期进行安全性分析验证的手段，可以从根本上提高软件的安全性，降低开发成本。

 

［1］IEEE STD 1474． 1—2004 IEEE standard for communications-based train control ( CBTC ) performance and functional requirements ［S］． New York: IEEE Vehicular Technology Society 2005．

［2］Henriksson A，Aman U，Hunt J． Improving software quality in safety-critical applications by model-driven verification［J］． Electronic Notes in Theoretical Computer Science，2005，133( 31) : 101-117．

［3］Mohagheghi P，Dehlen V，Neple T． Definitions and approaches to model quality in model-based software development-review of literature［J］． Information and Software Technology，2009，51 (12) :1646-1669．

［4］Giese H，Henkler S． A survey of approaches for the visual model-driven development of next generation software-intensive systems［J］． Journal of Visual Languages and Computing，2006，17( 6) : 528-550．

［5］Abdulla P A，Deneux J，Stalmarck G，et al． Designing safe，reliable systems using SCADE［C］/ / Proceedings of ISOLA’04． Springer-Verlag，2004．

［6］Faber J，Meyer R． Model checking data-dependent real-time properties of the European Train Control System［C］/ / IEEE Conferences on Formal Methods in Computer Aided Design．

2006: 76-77．

［7］Pretschner A，Ltzbeyer H，Philipps J． Model based testing in incremental system development［J］． Journal of Systems and Software，2004，70( 3) : 315-329．