属性驱动的列车控制系统需求建模与验证

2014-08-01何丽芸程瑞军

铁路计算机应用 2014年2期

关键词：控系统车载约束

何丽芸，赵林，程瑞军

（北京交通大学轨道交通控制与安全国家重点实验室，北京 100044）

属性驱动的列车控制系统需求建模与验证

何丽芸，赵林，程瑞军

（北京交通大学轨道交通控制与安全国家重点实验室，北京 100044）

形式化语言越来越多地用来描述列车控制系统需求规范，其精确的语法和语义一方面有助于创建精确的需求模型、消除理解差异，另一方面也为进一步分析验证提供了基础。通过提出一种基于属性的需求分析方法，利用具体的形式化技术来分析需求。首先将由自然语言描述的需求规范转换为属性描述语言（PSL）形式化规范，并通过仿真和博弈分别进行语义检查和可实现性验证，最后通过断言来检验形式化语言所刻画的系统的精确性和完整性。该方法从自然语言形式的需求约束中直接提取相关需求规范，构造形式化模型并进行验证，为需求的早期确认提供了一种新的实用途径。并以CTCS-3级列控系统RBC切换场景为例，说明该方法的有效性。

需求规范；验证；列车控制系统；仿真；可实现性

需求规范是系统开发重要的依据性规范标准。高质量的需求规范可以切断需求阶段的bug来源，如果需求规范的质量控制不到位，极有可能会产生最原始的bug，并将会贯穿到整个系统开发的始终，造成巨大的经济损失。工业数据显示大约50%的产品缺陷是由于需求的质量不到位造成的，大约80% 的返工工作量可以追溯到需求缺陷[1]，特别是对列车运行控制系统（以下简称“列控系统”）而言，其需求规范的缺陷往往造成不可估量的财产损失和人员伤亡。具体来说，列控系统需求规范大多都是依靠领域专家们的经验而制定的，不可避免地存在某些漏洞或者安全隐患；另外，用自然语言刻画的系统需求规范可能存在歧义。这都将会给系统的设计与开发带来不利影响。因此，在列控系统开发的早期阶段对需求进行形式化分析验证以保证需求质量显得十分必要。

列车运行控制系统是安全苛求系统。根据铁路工业标准（CENELEC EN50128[2]）和国际通用的安全相关系统标准（IEC61508[3]），对高安全系统（安全完善度等级4级），强烈推荐使用形式化方法对系统需求进行分析验证。形式化方法[4]是采用严格的数学语言、具有精确的数学语义的方法，适合于软件和硬件系统的描述、开发和验证。属性描述语言（PSL）[5]作为一种形式化的属性规范语言，易于读写、语法精简、语义严格清晰。利用PSL语言表达需求，使得需求以唯一的方式被解释，能够排除由自然语言带来地二义性，进而准确地表达需求。

因此，本文以PSL语言为基础，提出了一种基于属性的需求分析方法，该方法可以从自然语言形式的需求约束中直接提取和构造形式化模型，通过对形式化模型进行仿真（Simulation）、博弈（Game）、以及断言（Assurance）来分析需求，确保形式化需求的语义正确性、完整性以及可实现性。其中，设计人员可以通过属性仿真来构建具体的场景并检验某个属性所刻画的行为是否符合需求规范约束；通过博弈来对形式化模型进行可实现性验证；通过属性断言从更全面整体的角度来分析形式化模型，验证形式化属性集是否一致，是否足够完整地刻画一个系统的行为。从而可以有效地解决需求规范的表意模糊和逻辑缺陷问题，并且能够在系统开发的初期对规范中的漏洞进行排查，提高需求的质量。最后，本文以列控系统的无线闭塞中心（RBC）切换场景[6]为例来说明该方法的有效性。

1 基于属性的需求分析方法

基于属性的需求分析方法通过属性仿真、属性断言和博弈来对系统需求的一致性、完整性以及可实现性进行验证分析，是一个不断迭代的过程。图1描述了基于属性的需求分析过程。

如图1所示，设计人员首先从自然语言描述的用户需求或未经验证完善的需求规范中提取和构建形式化模型，通过属性仿真来探索和研究形式化属性的语义，将属性的形式化表达式逐级分解来使设计人员更好地理解表达式，也可以用来纠正PSL形式化属性表达式的错误；通过博弈来分析所刻画的系统是否存在，是否可实现；通过属性断言对形式化需求规范的一致性和完整性检查。其主要步骤简述如下：

图1 基于属性的需求分析过程

（1）从自然语言描述的用户需求或未经验证完善的需求规范约束中直接提取和构建形式化需求模型Γ，该形式化需求模型使用PSL表示。对需求模型Γ进行一致性检查，保证需求模型中的需求之间不存在冲突。

（2）若需求一致，则通过仿真来逐条检验需求模型Γ的形式化表达是否正确，是否描述的是所期望的行为，从而纠正并探索PSL形式化属性表达式的语义。

（3）检查由需求模型Γ所刻画的系统是否为可实现，即是否存在与之相一致的系统。需求模型Γ中的变量分为环境（不可控）变量和系统（可控）变量。需求包含假定（Assumptions）需求和保证（Guarantees）需求两种类型，分别是对环境变φ量和系统变量的约束。当环境输入变量满足所有假定需求时，存在一组满足所有保证需求的系统变量，则称该规范是可实现的。否则，规范为不可实现，需进行调试并修改该需求集。

（4）若系统可实现，则对形式化模型进行基于断言的验证，即通过两个属性集：assertionsφA和possibilities φP分别进行验证。assertions φA，验证所构建的形式化模型是否一定满足assertions属性，通过assertions来检查形式化模型是否约束不足。possibilities φP，验证形式化模型是否存在满足possibilities属性的可能性，通过possibilities来检查需求是否约束过强。

（5）如果不满足φA，检查需求模型Γ是否约束不足，是否需要增加系统行为约束。如果不满足φP，检查需求模型Γ是否约束过强，是否需要去除系统行为的某个约束。通过这种方法，对需求模型Γ检查修改，保证形式化需求模型的正确性。

（6）通过对需求模型Γ的修改更新，使其均满足φA和φP后，逐步增加两个属性集φA和φP中的属性约束再进行验证，转到第一步，不断迭代，从而丰富和完善对系统的属性刻画。

为了形象地说明基于属性的需求分析，将其用一个三元组来表示：

其中：

Γ：形式化需求模型，描述系统行为和环境行为。Γ=＜S,E,RG,RA＞，其中，S和E是变量的两个不相交集，S代表系统变量（受系统控制的变量），E代表环境变量（受环境控制的变量）。需求分为Guarantee需求和Assumption需求。Guarantee需求用RG表示，是关于系统变量的PSL属性集；Assumption需求用RA表示，是关于环境变量的PSL属性集。

φA：assertions属性集，用Γ来描述的系统行为必须保证满足assertion属性（系统属性的所有路径必须都满足assertions属性集），通过assertions来检查需求是否约束不足。

φP：possibilities属性集，用Γ来描述的系统行为允许possibilities属性（系统属性中存在一条路径满足possibilities属性），通过possibilitie来检查需求是否约束过强。

下面以仲裁器为例进行说明，仲裁器的部分需求表示如下：

其中，g1和g2是布尔型系统变量，表示总线授权给出响应。r1和r2是布尔型环境变量，表示对总线发送请求。RG1表示两个请求信号不能同时得到响应，RG2表示有请求最终会有响应，当S满足RG时，E满足RA，则系统是可实现的。同时，通过φA和φP来检验需求模型是否正确完整。

RATSY（ Requirements Analysis Tool with Synthesis[7]）是一种基于属性的需求分析工具，它为工程人员提供了仿真、断言和可实现性验证的环境。以PSL为输入语言，避免了复杂的建模过程，对获得正确的形式化需求规范起到重要作用。下面以RBC切换场景为例说明基于属性的需求分析方法在列控领域中的应用。

2 基于属性的需求分析方法在列控系统需求规范中的应用

CTCS-3级列控系统是基于全球铁路移动通信系统（GSM-R）的列车运行控制系统,通过车-地信息的双向传输实现列车的闭环控制, 有效地提高列车的运营效率。由于包含有大量的子系统且功能复杂，在开发过程中，正确地理解并建立系统需求规范是首要问题。尽管工业数据显示大约50%的产品缺陷是由于需求的质量不到位造成的，大约80%的返工工作量可以追溯到需求缺陷，但是对需求的分析手段却很缺乏，而借助计算机辅助分析手段建立形式化的需求规范是一种有效的途径。下面以RBC切换场景为例进行说明。

2.1 形式化需求模型的建立

场景可以用作分析与验证需求的有效工具，可以通过选择一组具有代表性的场景实例来对属性需求进行检验，以发现需求中存在的缺陷。一组具有代表性的场景实例应该既包含描述一些系统期望行为的场景，即期望场景，也包含描述一些系统不希望发生行为的场景，即异常场景。使用场景实例对需求进行验证和校验，期望场景可以验证需求的完整性，异常场景可以验证需求的正确性。

CTCS-3级列控系统主要运营场景包括注册与启动、注销、进出动车段、等级转换、行车许可、RBC切换、自动过分相、重联和摘解、临时限速、降级情况、灾害防护、调车作业、人工解锁进路、特殊进路共14个场景文件，其中RBC场景是CTCS-3级列控系统中最为重要和最具代表性的流程之一，

现对该场景需求进行分析研究。场景中表示的属性含义参见表1。

表1 场景中各属性的含义

为了叙述简单清晰，根据CTCS-3级列控需求规范，提取RBC切换运营场景的部分片段（两部电台都能进行正常的RBC切换）进行分析，以车载设备为系统，其他均看作环境。构建一个初步的形式化需求模型，该模型用形式化语言PSL表述如下：

RG1：允许车载设备与RBC 通信中断的时间为7 s～20 s，当超过这段时间则降级处理。always(CommunicationInterrupt=1&&C3=1-＞next (C2=1))

RG2：如果车载设备的版本与RBC的版本不兼容，则触发车载设备降级运行。

always(ID_RBCincompatible=1&&C3=1-＞next(C2=1))

RG3：当列车运行速度超过最大速度曲线规定的速度时，C3控制单元应能通过安全数字接口实现安全防护（超速时应能实现安全防护）。

always(OverSpeed=1-＞next(SafetyProtection=1))

RG4：当车载设备(OBE)正常运行无故障时，应能实现通信、安全防护、监控、制动和计算的功能。

always(OBE_faultFree＜_＞(!CommunicationIn terrupt&&SafetyProtection&&Supervision&&Brak e&&

Compute))

RG5：车载设备应处于CTCS-2或CTCS-3级运行，同时CTCS-2和CTCS-3级互斥。

always((C3=1&&C2=0)||(C3=0&&C2=1))

RG6：如果通信不中断且列车处于CTCS-3级运行，则继续以CTCS-3级运行。

always(CommunicationInterrupt=0&&C3=1-＞next (C3=1))

RA1：预告点（LTA）到切换点（RN）应满足列车不小于40 s的运行距离。

always(LTA=1_＞next[40](RN=1))

RA2：当列车前端通过RN时，“移交RBC”停止对列车的控制，切换到“接收RBC”进行控制。

always(RN=1_＞next(HandoverRBC_MA=0& &AcceptRBC_MA=1))

RA3：列车不能同时使用“移交RBC”发送的行车许可和“接收RBC”发送的行车许可。

never(HandoverRBC_MA&&AcceptRBC_MA)

RA4：为消除RBC切换对列车正常运行的影响，车载设备应设置两部独立GSM-R通信电台（GSM-R1和GSM-R2），车载设备通过GSM-R1接收“移交RBC” 发送的MA，通过GSM-R2呼叫“接收RBC”。

(always(HandoverRBC_MA＜-＞GSMR1))&&(always(AcceptRBC_MA＜-＞GSM-R2))

RBC切换描述了在不同RBC边界处，实现列车在两个RBC间行车许可控制的安全切换过程。通过上述的转化，初步得到一个形式化的需求规范如下：

PARBCTransition=＜Γ,φA,φP＞

其中，

S ={C3, C2, Speed_c2, Speed_c3,

OverSpeed, SafetyProtection, OBE_faultFree, SafetyProtection, Supervision, Brake, Compute }

E={CommunicationInterrupt, ID_RBCincompatible, LTA, RN, HandoverRBC _MA,AcceptRBC_MA, GSM-R1, GSM-R2 }

2.2 形式化模型的仿真、可实现性验证及断言

2.2.1 形式化需求的仿真

利用形式化属性成功地刻画系统的一个先决条件是对属性语言要有一个正确的理解。RATSY提供的属性仿真环境使得工程人员可以逐条对属性约束的正确性进行确认，从而判断该属性所描述的行为是不是我们所期望。例如，对属性RA2: always(RN-＞next(!HandoverRBC_MA&&AcceptRBC_MA))进行语义检验。仿真结果如图2所示，给出正例（RA2所描述的需求成立）和反例（RA2所描述的需求不成立），更好地理解满足属性RA2或违反属性RA2的情况。

图2 属性仿真

2.2.2 形式化需求模型的可实现性验证

在保证需求模型中的每条需求约束都正确后，开始从整体上对形式化模型进行可实现性验证。也就是说，当所有的环境变量满足Assumption需求时，所有的系统变量也满足Guarantee需求。只有保证需求模型是可实现的，后面的断言验证才有意义。通过验证，上面的需求是不可实现的。为了更加方便快速地找到需求不可实现的原因，工具为工程人员提供了诊断信息并且将与该系统不可实现有关的需求做标记。如图3所示，需求RG1、需求RG2、需求RG3、需求RG4以及需求RG6与系统的不可实现有关。RG6表示如果通信不中断且列车处于C3级运行，则继续以C3级运行，而RG2表示如果车载设备的版本与RBC的版本不兼容，则触发车载设备降级运行。可见两者存在矛盾，应在通信不中断并且车载设备的版本与RBC的版本兼容时，系统才可能以C3级正常运行。因此，对RG6进一步约束为：always(CommunicationInte rrupt=0&&C3=1&&ID_RBCincompatible=0_＞next( C3=1))。验证修正后的需求模型是可实现的。基于属性的需求分析方法为我们查找隐藏在需求中的可实现性问题提供了一种快捷而有效的手段。

图3 GAME窗口

2.2.3 形式化需求模型基于断言的验证

虽然我们保证了需求集的可实现性和属性语义正确性，但是这对于刻画一个完整而正确的系统是远远不够的，通过基于断言的验证来保证需求的完整性以及需求约束程度的合理性，约束不能过强或者不足。

前面所给的形式化模型中φA为空集，现在假定φA={a1, a2}并进行验证，其中：

a1：当车载设备通过两部电台与RBC1和RBC2同时进行连接通信时，如果司机关闭了驾驶台，车载设备将对RBC1和RBC2都执行终止任务程序。

always(DeskClosed=1-＞next(Handover-RBC_MA=0&&AcceptRBC_MA=0))

a2：如果列车位置信息无效，则降级，列车继续保持与RBC的通信会话

always(TrainLocation=0-＞next(C2=1))

验证结果如图4所示，需求集Γ=＜S,E,A,G＞不能满足φA属性，说明需求Γ约束不够，将a1和a2分别加入需求集Γ中，从而更新了需求集合，增强了对系统属性的约束，使得系统属性表示更加准确。

图4 验证结果

对φP集验证的意义不同于φA的验证，φA所描述的属性需求集Γ的所有路径必须都满足。而φP中的属性需求集Γ只要存在一条路径满足即可，保证了需求集约束的精确程度，不会因为约束过紧或约束不够而影响所刻画系统的准确性。在这里，φP={p1 },其中：

p1: 当列车RBC切换点时，通信中断，列车不能得到移交RBC和接收RBC的行车许可。

always(RN=1&&CommunicationInterrupt=0_＞next(HandoverRBC_MA=0&&AcceptRBC_MA= 0))。

验证结果表明，需求模型所刻画的系统满足p1属性，与我们的设计意图相符，说明需求约束并不存在过强的问题。

运用上面的方法进行不断迭代，发现列控需求规范中的缺陷和漏洞，例如某条需求可能存在约束不够或约束过强的问题，从而获得高质量的需求，也保证了生命财产的安全。

3 结束语

本文所提出的基于属性的需求分析方法通过验证需求的正确性、完整性以及可实现性，可以有效地解决需求规范的表意模糊和逻辑缺陷问题，并且能够在系统开发的初期对规范中的漏洞进行排查，提高需求的质量。采用该方法将PSL与可视化界面工具RATSY相结合，对高安全要求的列控系统需求规范进行分析验证，通过反例对错误进行定位和修改。验证过程表明，基于属性的需求分析方法适用于CTCS-3级列控系统需求规范的分析验证。该方法简便易行，避免了复杂的建模和转换过程。对于初步编写规范及对原有系统规范进行更新升级的工作具有重要的意义。

[1] 常云丽,邬欣明,郑威.军用软件需求分析研究[J].火力与指挥控制，2013，38（1）.

[2] CELENEC EN 50128: Railway Applications - Communications, signaling and processing systems- Software for railway control and protection systems[S]. 2001.

[3] International Standard IEC 61508: Functional Safety of Elec

trical/Electronic/Programmable Electronic SafetyRelated Sys

tems. International Electrotechnical Commission[S]. 2000. [4] 包丽梅,张玉春,张世铮.关于形式化方法与软件可靠性的研究[J].内蒙古民族大学学报：自然科学版，2010（2）：166-167.

[5] Accellera. Property specif i cation language reference manual version 1.1[EB/OL]. (2004-06-09)[2008-03-02]. http://www. eda.org/vfv/docs/PSL-v1.1.pdf．

[6] 中华人民共和国铁道部. CTCS-3级列控系统系统需求规范(SRS)[M]. 北京：中国铁道出版社，2009.

[7] Bloem R, Cavada R, Cimatti A ,et al. RATSY-A new Requirements Analysis Tool withSynthesis[C].Computer Aided Veri-f i cation, 22nd International Conference. Berlin:Springer-Verlag, 2010: 425-429.

责任编辑杨利明

Property-driven modeling and verif i cation for requirements of Train Control System

HE Liyun, ZHAO Lin, CHENG Ruijun
( State Key Laboratory of Rail Traff i c Control and Safety, Beijing Jiaotong University, Beijing 100044, China )

Formal languages were increasingly used to describe the requirements specif i cation of Train Control System, the precise syntax and semantics on the one hand, helped to create accurate demand model, eliminated understanding differences, on the other hand also provided a basis for further analysis of the validation. This paper presented a property based requirements analysis approach which analyzed requirement by the application of specialized formal analysis techniques. Firstly, requirements described by natural language were transformed into formal requirements described by PSL (Property Specification Language). Secondly, the semantics were checked by simulation and the realizability of the System was verif i ed by the game. Finally, the correctness and completeness of the System were validated by assurance. This method directly extracted the relative requirements specif i cation from requirement constraints described by natural language and formalized the structures model to verify, also provided a new practical way for the early validation of the requirements. By using some requirement fragments from RBC Handover scenarios of CTCS-3 Train Control System as a realistic example, it was demonstrated the effectiveness of this approach.

requirements specif i cation; verif i cation; Train Control System; simulation; realizability