王海峰 杨旭文 刘 朔 刘 超

(北京交通大学电子信息工程学院 北京 100044)

1 研究背景

近年来，随着轨道交通的蓬勃发展，为确保列车运行安全和提高运输效率，基于通信的列车运行控制(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系统安全苛求软件开发方法。

2 ZC系统

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

2.1 亦庄线项目概况

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

图1 北京地铁亦庄线线路

2.2 ZC系统体系结构

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

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

图2 ZC系统双版本容错结构

3 ZC系统建模方法

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

3.1 MA 计算

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

图3 移动授权原理

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

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

3.2 列车管理

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

图4 MA计算模型主节点

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

图5 列车状态转移

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

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

4 系统安全性保障方法

图6 列车管理状态机模型

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

4.1 模型覆盖率

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

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

图7 模型覆盖率分析

4.2 形式验证

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

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

图8 ZC系统形式验证

5 结语

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

［1］IEEE STD 1474.1—2004 IEEE standard for communicationsbased 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-criticalapplications 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.