铁路计算机联锁系统安全关键软件的安全性能建模方法

李　耀,张亚东,郭　进,晏　姗,饶　畅，曹雅鑫

(西南交通大学 信息科学与技术学院，四川 成都　610031)

铁路信号是保障行车安全的重要基础设备，许多铁路信号系统软件都是典型的安全关键软件(Safety Critical Software)[1]，对安全性要求极为严格。安全性包括安全功能和安全性能两个方面。安全功能主要指“系统满足安全约束”及“构件或子系统失效对系统安全的影响”。安全性能包括安全完整度及风险等级等；安全完整度是指“系统在规定的条件下和规定的时间内完成安全功能的可能性”，风险等级是指“危害发生的概率及严重等级”[2-3]。现有的形式化建模方法缺乏对系统状态、行为及风险之间度量关系的描述，进行安全性分析时需要分别建立安全功能分析模型和安全性能分析模型，由于两者使用的建模方法不同，容易出现模型表达不一致或彼此不理解对方模型的问题。

传统的形式化方法，如自动机(Automata)，马尔可夫决策过程(Markov Decision Processes，MDP)和马尔可夫链(Markov Chain，MC)等，能够为软件设计提供统一的描述机制，但无法同时满足安全功能及性能分析建模需求，且“平坦”的建模结构导致模型复杂。文献[4]在有限确定的Automata的基础上提出了概率自动机(Probabilistic Automata，PA)方法，用于描述系统的概率行为。文献[5]在UML状态图(UML Statecharts)中引入概率特性，提出P-状态图(P-Statecharts)建模方法，支持不确定性分析，并具有层次性的优点。文献[6]针对系统概率不易确定的问题，提出确定性频率有限自动机(Deterministic Frequency Finite Automata，DFFA)方法，并给出了转化为确定性概率有限自动机(Deterministic Probabilistic Finite Automata，DPFA)算法，采用确定性的方式描述系统的度量关系。文献[7]为Automata的状态和变迁增加了“价格”特性，提出价格时间自动机(Priced Time Automata，PTA)方法，能够反映系统响应过程中的消耗关系。文献[8]针对铁路信号系统提出一种关联系统功能和风险等级的确定性的安全行为建模方法，反映了系统响应时风险等级的变化情况。PA，P-Statecharts和DFFA能够描述铁路信号系统安全完整度，PTA和安全行为方法能够描述系统的风险等级，但PA，DFFA，PTA及安全行为方法均采用“平坦”的建模机制，不具有层次性，且不能同时满足安全完整度和风险等级的建模需求；P-Statecharts受限于Statecharts语法，不能完全从根本上消除不确定性，且采用优先级的机制导致模型复杂。同时，PA和P-Statecharts属于不确定性的建模方法，与铁路信号系统安全功能所要求的确定性存在分歧。

SyncCharts[9]是Charles André针对反应式系统提出的一种高效、清晰、确定的图形化建模语言，具有层次性、并发性和优先级抢占的特点，支持软件安全功能分析建模，但不能进行定量计算，无法满足铁路信号系统安全关键软件安全性能分析建模的需求。因此，本文在SyncCharts的状态和变迁中增加转移频数和失效后果严重度2个参数，提出频率风险SyncCharts建模方法和模型分析方法；以铁路计算机联锁系统中的信号请求子系统为例，建立该子系统安全关键软件安全性能分析模型，计算模型状态的激活概率和风险等级，定量描述该子系统关键软件的安全性能。

1　频率风险SyncCharts建模方法

首先定义频率风险SyncCharts的基本结构单元：频率风险状态转移图(DFRSTG)；然后在此基础上给出频率风险SyncCharts的定义、约束条件和宏步规则。

1.1　频率风险SyncCharts定义

DFRSTG是一个具有唯一初始状态、基于事件响应的状态转移图。DFRSTG的状态和变迁具有转移频数特性，表示保持原状态和触发变迁的次数。状态具有失效后果严重度的特性，表示该状态失效后导致的系统后果严重度的等级。变迁具有变迁类型属性，类型集记为TTYPE::={TSTRONG,TWEAK,TSYNC}，其中TSTRONG为强变迁，TWEAK为弱变迁，TSYNC为同步变迁。

定义1 ：八元组(S,s0,Sf,G,T,f,a,r)称为DFRSTG。其中：

S为有限状态集；

s0∈S为缺省状态；

Sf⊆S为终止状态集；

G为可接受或产生的有限原子事件集；

T⊆S×α×TTYPE×TLABEL×S为变迁集；α∈N+为转移优先级；TLABEL::=G×G为变迁标号集，表示触发变迁的事件和产生的动作；

f:S∪T→N+为频数函数，给状态和变迁分配频数；

a:S→2A×G为状态动作函数，其中A::={AENTER,AIN}，AENTER和AIN分别表示进入、处于状态时需要产生的动作；

r:S→{CL1,CL2,CL3,CL4}为失效后果严重度的函数，用于给状态分配失效后果严重度的等级，其中CL1，CL2，CL3，CL4分别表示可忽略的、容许的、不希望的和不容许的等级，且有CL4>CL3>CL2>CL1。

定义2： 四元组(S,stop,D,ρ)称为频率风险SyncCharts模型，记为DFRSC。其中：

stop∈S为根状态，且sTYPE(stop)=SMACRO；

D为DFRSC包含的有限DFRSTG集；

ρ:S→2D为DFRSTG分配函数，且∀s∈S·ifsTYPE(s)=SBASICthenρ(s)=∅ elseρ(s)≠∅。

根据定义2，DFRSC的层次结构是以stop为根，以SMACRO状态为中间节点，以SBASIC状态为叶子节点的1个层次树。

DFRSTG中，变迁t∈T的源状态记为σ(t)， 目标状态记为τ(t)。 对任意SMACRO状态s2，s2包含的频率风险状态转移图dFRSTG∈D，有∀s1∈dFRSTG.S，称s1为s2的孩子，简记为s1∈ρ(s2)；称s2是s1的双亲，记为s2=η(s1)。ρ(s)的自反传递闭包ρ*(s)::=ρ(s)∪∪{s1:ρ*(s)·ρ*(s1)}表示s的孩子集合。DFRSTG的状态有多条变迁时，每条变迁的优先级不同，且强变迁的优先级最高，同步变迁的优先级最低。

DFRSC的层次性使得DFRSC所有状态均为stop的孩子状态，且状态的父子关系不存在循环，变迁不能跨越状态层次；TSYNC变迁的源状态为SMACRO状态，且包含的DFRSTG均有至少1个终止状态，具体满足以下约束：

(1)∀s:Sstop·s∈ρ*(stop)；

(2)∀s,s1,s2:S·ifs1=η(s),s2=η(s)，thens1=s2；

(3)∀s:S,s∉ρ*(s)；

(4)∀t:T·η(σ(t))=η(τ(t))；

(5)∀t:T·ift.TTYPE=TSYNCthen

sTYPE(σ(t))=SMACRO∧∀dFRSTG:DFRSTG∈ρ(σ(t))·dFRSTG.Sf≠∅∧ ∀t1:T·ift1≠t,σ(t1)=σ(t) thent1.TTYPE≠TSYNC。

1.2　DFRSC宏步规则

DFRSC从1组格局转移到下一组格局的过程称为1个宏步。宏步反映了DFRSC对事件的计算过程。

格局为DFRSC的1组稳定状态集，DFRSC的格局集合记为o(DFRSC)。初始格局表示DFRSC默认状态集，记为o0(DFRSC)。 对DFRSC的任意一组格局u∈o(DFRSC)，stop∈u； 同时∀s:S∈u·ifstype(s)=SMACROthen ∀dFRSTG:DFRSTG∈ρ(s)， ∃1s1∈dFRSTG.S·s1∈u。

SyncCharts中，状态及其所有出发变迁构成反应细胞。DFRSC在SyncCharts反应细胞的基础上增加了转移频数和失效后果严重度这2个参数，但不改变SyncCharts的确定性原则，转移过程满足SyncCharts的宏步规则[9]，即DFRSC在当前格局下，以反应细胞为核心，根据细胞的层次结构、反应细胞变迁类型及优先级，依照SyncCharts宏步规则计算下一组稳定状态。

由于DFRSC的层次性，同一组格局激活不同层次上的反应细胞，将导致格局转移到不同的稳定状态。宏步规则中未被激活的反应细胞称之为休眠细胞EDRC，激活的反应细胞称之为激励细胞ERRC，其中保持原状态的激励细胞记为EHRC，触发变迁的细胞记为ETRC。DFRSTG的1组格局u满足u=EHRC.s∪ETRC.s∪EDRC.s，且EHRC.s∩ETRC.s=∅，ERRC.s∩EDRC.s=∅。

2　DFRSC模型分析

MDP[10]是描述系统随机性和不确定性的基本结构之一，具有成熟的模型分析方法[11]。将DFRSC转化为等价的MDP，再通过MDP的模型分析方法实现DFRSC的模型分析。

定义3：DFRSC的格局序列hu=u0,u1,u2,u3，…称为DFRSC的路径，记为h(DFRSC)。且有

(1)u0=o0(DFRSC)；

(2) ∀i>0,ui+1∈n(ui)。

n(ui)为格局u的可达格局集合。DFRSC路径为DFRSC从初始格局开始可能的执行过程的格局序列。

定义4： 四元组(S,s0,p,w)称为MDP模型，记为DMDP。其中有

w:S→N+为成本函数。

定义5：DMDP上的1个状态序列hs=s0,s1,s2,s3，…称为DMDP的路径，记为h(DMDP)，且∀i>0，p(si+1|si)>0。

S′=o(DFRSC)；

p′=S′×S′→R，如果：

(1)∃s1,s2∈S′·ifp′(s2|s1)>0，∃u1,u2∈o(DFRSC)， thens1=u1，s2=u2，u2∈n(u1)，p′(s2|s1)=p′(u2|u1)；

(2)∃u1,u2∈o(DFRSC)，ifu2∈n(u1)，then ∃s1,s2∈S′,s1=u1,s2=u2，p′(s2|s1)>0，p′(s2|s1)=p′(u2|u1)；

w′:S′→N+，且∀s1∈S′·∃1u1∈o(DFRSC)·s1=u1,w′(s1)=r(u1)。

m(DFRSC)定义了DFRSC向DMDP结构的转移关系，表明DFRSC的格局集和DMDP结构的状态集有相同的状态空间。T和p分别描述了DFRSC和DMDP的转移关系，表明DFRSC和DMDP具有相同的执行路径。

定理2： 设Ψ是DFRSC的路径u0,u1,u2，…向DMDP路径s0,s1,s2,…的映射，则∀hs∈h(m(DFRSC))⟺∃hu∈h(DFRSC):Ψ(hu)=hs。

证明：根据定理1，m(DFRSC)将DFRSC映射为DMDP，DFRSC的格局集对应DMDP的状态集。∀s1,s2∈S，如果p(s2|s1)>0，则DFRSC中∃u1,u2∈o(DFRSC)，u1=s1，u2=s2，u2∈n(u1)。故MDP的任意路径hs=s0,s1,s2，…均对应DFRSC的1条格局路径hu=u0,u1,u2，…。

假设∃hu∈h(DFRSC)，Ψ(hu)=hs， 但s′∉h(m(DFRSC))。 根据定理1有：hu=u0,u1,…,ui,ui+1，…，且∃i,ui+1≠n(ui)， 否则hs∈h(m(DFRSC))。 但如果存在此(ui,ui+1)， 则hu∉h(DFRSC)。 故DFRSC中的任意路径hu=u0,u1,u2，…对应DMDP的1条路径hs=s0,s1,s2，…。

定理2表明DFRSC和DMDP结构同构，有相同的状态序列和转移关系，如图1所示。

图1　DFRSC与DMDP算法同构示意图

DFRSC转换为DMDP的算法原理为：将DFRSC的格局转换为DMDP结构的状态；计算DFRSC格局的最大失效后果严重度，将该严重度转化为DMDP对应状态的成本；将DFRSC的频数转化为DMDP的概率。该算法如图2所示。图2中：f(ei.s)为反应细胞ei状态的频数；f(ei.t)为变迁t的频数。

采用PRISM[12]模型分析工具对DMDP模型进行分析，得到DMDP的转移概率和即时期望成本；这2个量就是DFRSC模型的激活概率和风险等级；用这2个量则可以定量描述铁路信号子系统安全关键软件的安全性能。

3　计算机联锁系统的DFRSC建模

3.1　信号请求子系统的DFRSC模型

铁路计算机联锁系统是一个对安全功能和性能要求严格的系统。以计算机联锁系统[13]的信号请求子系统为例建立DFRSC模型，通过DFRSC模型定量分析信号请求子系统各个状态的转移频率，识别系统的风险等级。信号请求子系统的工作流程为：信号请求子系统接收到信号请求时，检查道岔是否选排一致；若没有选排一致，则转换道岔使道岔到其需求位置，若转换道岔失败，则放弃信号请求；若选排一致或道岔转换到需求位置后，如果进路内首区段空闲，或首区段故障但开放引导信号，则信号请求成功，广播安全请求消息给其他子系统[14]。在计算过程中，如果DSignal模型接收到取消信号，则模型立即重置；若通信中断，则DSignal模型进入安全防护状态。该系统涉及8个事件，事件名称及其含义见表1。

图2　DFRSC转换为DMDP算法

事件含义事件含义g1信号请求　　g2道岔选排一致g3道岔转换超时g4首区段空闲　g5引导信号　　g6取消信号　　g7通信中断　　g8安全信号请求

信号请求子系统的DFRSC模型如图3所示。在图3中，IN:g8表示处于该状态时广播消息g8；s1(CL3/50)表示r(s1)=CL3，f(s1)=50； 50/g1表示转移频数为50，转移条件为g1发生；变迁①表示变迁的优先级为1；状态s0，s1，s2，s3，s4，s5，s6，s7分别表示选排判断、等待信号请求、接受信号请求、道岔选排不一致、道岔选排一致、正常安全信号请求、首区段故障下安全信号请求和通信中断后的故障状态。

图3　信号请求子系统的DFRSC模型

根据定义2，信号请求子系统DFRSC模型的定义如下。

DSignal=(S,stop,D,ρ)，其中：

S={DSignal,s0,s1,s2,s3,s4,s5,s6,s7}；

stop={DSignal}；

D={s8,s9}；

ρ(DSignal)={s8},ρ(s0)={s9}；

s8=((s0,s7),s0,∅,(g6,g7),((t1:s0,1,

TSTRONG,(g6,∅),s0),(t2:s7,1,

TSTRONG,(notg7,∅),s0),(t3:s0,2,

TSTRONG,(g7,∅),s7)),f(s0)=100,

f(s7)=1,f(t1)=2,f(t2)=2,f(t3)=

3,a(s0)=a(s7)=∅,r(s0)=CL3,

r(s7)=CL4)；

s9=((s1,s2,s3,s4,s5),s1,∅,(g1,g3,g4,g5,g8),((t1:s1,1,TSTRONG,((g1,∅),s2),(t2:s2,1,TSTRONG,((notg2,∅),s3),(t3:s3,2,TSTRONG,(notg3,∅),s1),(t4:s2,2,TSTRONG,(g2,∅),s4),(t5:s3,1,TSTRONG,(g3,∅),s4),(t6:s4,1,TSTRONG,(g4,∅),s5),(t7:s4,2,TSTRONG,(notg3andg5,∅),s6),f(t1)=50,f(t2)=10,f(t3)=1,f(t4)=40,f(t5)=9,f(t6)=46,f(t7)=3,f(s1)=50,f(s5)=46,f(s6)=3,f(s2)=f(s3)=f(s4)=0,a(s1)=a(s2)=a(s3)=a(s4)=∅,a(s5)=a(s6)=(IN,g8),r(s1)=r(s2)=r(s3)=r(s4)=CL3,r(s5)=r(s6)=CL4)。

3.2　Signal模型分析

图4　Signal模型的DMDP模型

利用PRISM[14]对图4所示的DMDP模型进行分析。利用PRISM的实验机制，分析状态s0，s1，s2，s3，s4，s5，s6，s7在DMDP的10个执行周期中的激活概率，如图5所示。由图5可知：状态s2，s4，s5的激活概率较大，表明信号请求子系统经常运行在接收信号请求、道岔选排一致、满足安全条件这3个状态，因此为降低信号请求子系统的可容忍危害概率，保证子系统的安全性能，在对信号请求子系统进行设计和测试时需要对这3个状态进行重点分析。选取DMDP执行第1～10个执行周期，分析信号请求子系统在10个执行周期中的风险等级变化情况，如图6所示。由图6可知：在8个执行周期后，风险等级逐步稳定在3.8。根据EN50128[15]的风险管理可知，信号请求子系统的风险等级较高，因此应采取相关技术措施对该子系统进行风险控制和管理，保证子系统的风险等级满足安全性能的要求。

图5　Signal状态激活概率与执行周期的关系

图6　Signal风险等级与执行周期的关系

由此可见，采用频率风险SyncCharts模型和模型分析方法，对信号请求子系统安全关键软件的安全性能进行分析，可以辨识出子系统经常运行的状态和风险等级，从而指导软件系统的优化设计、重点测试和维护，为系统的风险控制和管理提供定量参考，保障软件满足安全性能的要求。

4　结　语

本文通过在SyncCharts建模方法中增加转移频数和失效后果严重度2个参数，提出1种铁路信号安全关键软件安全性能建模的频率风险SyncCharts方法，给出了频率风险SyncCharts的定义、约束条件和宏步规则；为对频率风险SyncCharts进行模型分析，给出了将频率风险SyncCharts转化为MDP的算法，通过对MDP模型进行分析，实现对频率风险SyncCharts模型的分析。以铁路计算机联锁系统中信号请求子系统安全关键软件为例，分析得到铁路信号子系统的激活概率和风险等级2个安全性能指标，定量描述该子系统关键软件的安全性能，为软件的优化设计、重点测试和维护提供定量参考，从而为系统的风险控制和管理提供定量参考，保障软件满足安全性能要求。本文提出的方法已在CBTC联锁系统软件设计及开发中得到应用，实践表明该方法对信号子系统安全关键软件安全性能的设计、测试和风险管理具有一定的指导意义。

[1]DAVID L Parnas，A John van Schouwen，SHU PO Kwan. Evaluation of Safety-Critical Software[J]. Communications of the ACM, 1990, 33(6):636-648.

[2]CENLEC.EN50126 Railway Applications—the Specification and Demonstration of Reliability，Availability，Maintainability and Safety(RAMS) [S].Geneva：International Electrotechnical Commission，2002.

[3]白鑫, 王阳, 郭湛. 基于EN50126标准的铁路联调联试安全分析[J]. 中国铁道科学, 2011, 32(4):104-108.

(BAI Xin，WANG Yang，GUO Zhan.Safety Analysis on System Integration Test and Commissioning for Railway Based on EN50126 Standard[J]. China Railway Science, 2011, 32(4):104-108. in Chinese)

[4]MICHAEL O RABIN. Probabilistic Automata [J]. Information and Control, 1963, 6(3): 230-245.

[5]DAVID N Jansen，HOLGER Hermanns，JOOST-PIETER Katoen. A Probabilistic Extension of UML Statecharts[C]//Formal Techniques in Real-Time and Fault-Tolerant Systems. London: Springer Berlin Heidelberg, 2002: 355-374.

[6]COLIN de la Higuera. Grammatical Inference: Learning Automata and Grammars [M].New York: Cambridge University Press, 2010: 329-353.

[7]GERD Behrmann，KIM G Larsen，JACOB I Rasmussen. Priced Timed Automata: Algorithms and Applications[C]//Formal Methods for Components and Objects. Leiden: Springer Berlin Heidelberg, 2005: 162-182.

[8]喻钢, 刘晓文, 熊静, 等. 高速铁路列控中心软件安全性需求形式化建模[J]. 铁道学报, 2013, 35(7): 74-79.

(YU Gang，LIU Xiaowen，XIONG Jing，et al. Formalized Modeling of Safety Requirements of High-Speed Train Control Center Software System[J]. Journal of the China Railway Society, 2013, 35(7): 74-79. in Chinese)

[9]CHARLES André.Semantics of SyncCharts[M].Nice: University of Nice Sophia Antipolis，2003: 1-76.

[10]TOMAS Brazdil，KRISHNENDU Chatterjee，MARTIN Chmelik，et al. Verification of Markov Decision Processes Using Learning Algorithms[J]. Computer Science, 2015, 8837:98-114.

[11]CHRISTEL Baier, JOOST Pieter Katoen. Principles of Model Checking[M]. Massachusetts: The MIT Press, 2008: 832-899.

[12]MARTA Kwiatkowska，GETHIN Norman，DAVID Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach[J]. International Journal on Software Tools for Technology Transfer, 2004, 6(2):128-142.

[13]杨扬, 潘明, 何梅芳. 联锁软件的Petri网形式化定义[J]. 中国铁道科学, 2002, 23(3):49-54.

(YANG Yang，PAN Ming，HE Meifang. Formal Specification of the Interlocking Software Using Petri Nets[J]. China Railway Science, 2002, 23(3):49-54. in Chinese)

[14]杨淘. 基于CBTC系统的联锁逻辑研究[D]. 成都：西南交通大学，2014.

(YANG Tao. The CBTC Based Interlocking Logic Research [J]. Chengdu：Southwest Jiaotong University，2014. in Chinese)

[15]BSI Standards Publicaiton. BS EN 50128:2011 Railway Applications-Communication，Signaling and Processing Systems-Software for Railway Control and Protection Systems [S].Geneva：International Electrotechnical Commission, 2011.