2020, Vol. 31
2. 卡斯柯信号有限公司, 上海 200071
2. CASCO Signal Co., Ltd., Shanghai 200071, China
基于通信的列车控制系统(communication based train control, 简称CBTC)是用来保证轨道交通安全、高效运行的控制系统.它打破了传统的轨道交通领域的固有限制, 可以在更精确的运行间隔中追踪列车, 已经成为我国轨道交通信号系统选型的主流制式[1].区域控制器(zone controller, 简称ZC)是CBTC系统的重要组成部分, 负责控制多个车站之间的一部分轨道上的列车及所涉及到的设备, 其核心功能是计算所控制的所有列车的移动权限(MA), 并将计算结果发送给相应的列车.在我们与卡斯柯信号有限公司的合作项目中, ZC系统还具有其他功能, 例如计算列车的安全位置、对区域内的列车进行分类以及更新轨道占用状态等.
作为CBTC的地面核心子系统, ZC的安全性直接关系到整个系统的成败.据统计, 在安全攸关系统的安全类问题中, 软件需求缺陷导致的问题已占到60%~80%[2], 需求类错误占到软件缺陷和错误的70%[3], 美军四代战机F-22项目办公室认为, 这一数字甚至高达85%[3].所以, 对安全攸关场景下的ZC系统进行安全需求的建模与验证至关重要, 是必须解决的问题.常见的需求验证包括需求的正确性、一致性和可满足性[4].本文关注需求的可满足性, 特指验证规约是否满足需求.在轨道交通的国际标准EN50128[5]、EN50129[6]中, 强烈推荐在软件开发生命周期的每部分使用形式化方法.因此, 有必要对ZC的安全需求进行形式化建模与验证.但在建模与验证过程中, 需要解决以下问题.
(1) ZC本身的复杂度:根据文献[7], ZC可以分为大约20个子系统, 在实现中可以进一步分为更多的子模块, 这些模块与不同的设备交互.所谓设备, 我们指的是与ZC(子)系统交互的外部实体, 不仅包括信号灯等物理世界中的设备, 而且包括计算机联锁系统等现有软件, 以及虚拟列车保护(VTP)等虚拟节点.根据IEEE1474.1标准[8], ZC可以与1 000多个这样的设备交互.由于设备在形式化的验证中由一组变量表示, 一个设备可能有数千个可能的值.所有这些值使得系统的模型过于庞大, 无法由现有的验证器进行计算, 导致了状态爆炸问题的出现.
(2) 形式化方法难以应用:形式化方法是使用一套明确定义的数学概念的符号来书写, 有严格的语法规范和确定的语义定义, 对数学基础的要求较高, 因此其学习成本较高, 非专业人士难以应用.在轨道交通领域, 涉及很多的领域知识, 对这类系统进行形式化, 不仅要求分析员有着深厚的形式化方法的知识, 也要熟悉领域知识.但通常来说, 领域专家不了解形式化, 而形式化专家缺乏充分的领域知识, 很难对ZC这类系统的安全需求进行直接的形式化建模与验证.
在现有的安全需求验证工作中, 主要有两种方式:一种是将安全需求直接建模为形式化语言并进行形式化验证, 例如文献[9]中使用ANSI/ISO-C规范语言(ACSL)将其形式化并实现自动化验证, 文献[10]中使用SCADE进行形式化的建模与验证, 文献[11]将Petri网与基于域的上下文推理相结合来实现形式化建模并最终实现验证等, 但是这些工作都无法避免非专业人士难以使用形式化方法的难题; 另一种就是基于半形式化需求模型的验证, 例如文献[12]中使用UML进行建模并用BACH进行验证, 文献[13]中使用SysML/KAOS进行建模并用Rodin进行验证, 文献[14]中使用消息顺序图进行建模并用UPPAAL进行验证等.这些半形式化模型最终都将转换为形式化语义模型进行验证.这类方法使用UML等图形化语言, 降低了形式化方法的使用成本, 但是并不能直接应用到ZC系统中, 它也没有处理验证问题的复杂性.总之, 现有的工作并不能解决全部解决上述问题.
因此, 本文提出一种安全需求的自动验证方法, 使用半形式化的问题框架方法(PF)[15, 16]来建模安全需求, 根据需求模型自动生成安全需求验证问题模型, 并根据需求模型和验证问题模型中的每个部分自动生成SCADE[17]工具中的Scade语言模型进行组合验证, 有效降低验证复杂度.选择PF有两个原因:(1) PF是一种基于环境建模的需求工程方法, 它将需求映射为环境(如ZC中的设备)中预期的变化, 特别适合建模ZC这类系统[18]; (2) PF使用投影进行问题分解, 能够有效降低需求问题的复杂度, 我们前期的工作[19]就提出了一种基于情景的自动投影方法.选择SCADE工具是因为它是一种典型的模型驱动开发支持工具, 常用于支持安全关键系统开发的整个过程, 涵盖了从建模、仿真到验证.它通过了轨道交通标准EN 50128认证, 达到SIL 3/4[5, 6], 能够减少开发过程中的成本、风险并能缩短验证所需的时间, 在轨道交通领域被广泛应用.
本文首先利用PF(problem frames)中的问题图和情景图建模ZC的安全需求问题, 并利用文献[19]中的自动投影方法将安全需求分解为若干个较小的子问题, 根据每个子问题的需求模型自动生成安全需求的验证问题模型; 然后, 根据需求模型和验证问题模型自动生成Scade模型并进行需求可满足性的组合验证.围绕上述工作, 本文第1节介绍本文涉及到的PF和SCADE验证方法.第2节对区域控制器(ZC)的安全需求使用PF进行建模与分解, 在一定程度上缓解状态空间爆炸的问题.第3节提出安全需求验证问题模型自动生成并转化为Scade模型的方法, 并由此生成ZC的验证模型.第4节以ZC的核心功能之一的移动授权终点计算子系统CAL_EOA为例, 将本文所提出的方法应用到实际的工业案例中, 实现对安全需求的建模、分解与自动验证过程.第5节介绍相关工作, 最后第6节总结全文并提出下一步工作.
1 预备知识 1.1 问题框架方法问题框架方法(PF)是Jackson提出的一种以环境为视角的需求工程方法[15, 16].它强调对与软件系统相交互的现实世界(即环境)进行刻画, 将需求的含义指称到对现实世界相关领域的描述上.其建模的基本概念是现实世界的“问题领域”, 以及软件系统与领域的“交互”.它使用问题图[16]来对需求进行静态的描述, 使用情景图[19]刻画如何动态实现需求.
在问题图中, 用领域(domain)、需求(requirement)和交互(interaction)来对问题进行描述, 其中, 领域可以被分为两类:机器领域(machine domain)和问题领域(problem domain).机器领域与问题领域之间共享的现象称为交互.交互分为两种类型:行为交互为机器领域和问题领域之间的接口交互(interface), 期望交互为问题领域和需求之间的引用(reference)以及需求与问题领域之间的约束引用(constraint).根据文献[16], 需求问题P可以定义为一个四元组:P=〈M, E, IS, R〉, 其中, 机器领域M表示要开发的软件; 环境领域E是所有与M交互的物理实体的集合; IS为交互(interaction)集; R是一组需求, 通常用自然语言描述.而交互可以定义为一个三元组:Interaction=〈Init, Recv, Phe〉, Init为交互的发送方, Recv为交互的接收方, Phe为共享的现象.具体细节详见文献[15].
情景图是交互流, 表示交互之间的关系.其基本表示采用活动图的形式.每个情景图都可以从3部分来理解:行为交互部分、期望交互部分以及行为交互和期望交互的使能关系部分.在行为交互部分中, 用活动图来对行为交互的变化流程进行描述, 用行为序关系(BehOrder)来描述行为交互之间的先后关系; 在期望交互部分中, 同样使用活动图来对期望交互的变化流程进行描述, 用期望序关系(ExpOrder)来描述期望交互之间的先后关系; 而在使能部分中, 可以使用行为交互和期望交互之间的连接来表示交互之间的使能关系, 包括同步关系(Syn)、行为使能关系(BehEna)和期望使能关系(ExpEna).根据文献[19], 情景图可以定义为一个三元组Scenario= 〈NodeSet, AssSet, FlowSet〉, 其中, NodeSet=IntSet∪CtrlSet表示节点集合, 可以分为两类:交互节点(IntNode)和控制节点(CtrlNode).其中, 交互节点包括行为交互(BehIntNode)和期望交互(ExpIntNode); 控制节点可分为以下5种:开始节点(StartNode)、结束节点(EndNode)、决策节点(DecisionNode)、合并节点(MergeNode)和分支节点(BranchNode).AssSet={AssType(inti, intj)|inti, intj∈IntSet}表示交互之间的关系, 包括以下5种类型:行为使能关系BehInt→ExpInt(BehEna)、行为序关系BehInt→BehInt(BehOrd)、同步关系BehInt↔ExpInt(Syn)、期望使能关系ExpInt→BehInt(ExpEna)和期望序关系ExpInt→ExpInt(ExpOrd).FlowSet={CtrlFlow(ctrli, nodej)|ctrli∈CtrlSet, nodej∈NodeSet}表示控制节点和其他节点之间的转换关系.具体细节详见文献[19].
1.2 SCADE Suite工具SCADE Suite[17]是ANSYS公司嵌入式软件家族中的一个产品线.它整合了形式化建模语言Scade, 内置了由Prover公司开发的模型检验器Design Verifier, 可以对Scade模型进行形式化验证.它是一个对关键应用进行综合设计的环境, 可以进行模型驱动设计, 被用于设计关键软件, 例如飞行控制系统、自动驾驶系统、轨道联锁系统、自动列车操控系统、紧急刹车系统、超速保护系统、列车空位检测系统以及其他众多航空航天、轨道交通、自动化领域的工业应用.除此之外, 它还支持仿真、验证和代码生成.
在Scade中, 模型的基本结构是操作符, 不同的操作符之间支持并行或嵌套的关系, 每个操作符需要定义它的名称、输入变量、输出变量和本地变量.不同的操作符之间通过实体线连接, 表示数据的传输路径.也就是说, 一根实线两端分别连接一个操作符的输出变量和另一个操作符的输入变量.在对模型进行验证时, 在被验证模型之外, 需要增加一个操作符观察者(observer), 用来描述所需要验证的性质.性质的描述语法和建模一样, 仅要求输出结果为一个布尔变量.
2 区域控制器的安全需求建模与分解ZC是CBTC系统的地面核心子系统, 其核心功能是用来计算列车的移动权限(MA), 对于CBTC系统起着至关重要的作用.根据PF中的问题定义, 首先获取待开发的软件ZC为机器M.ZC子系统通过车-地设备的无线通信实现车-地双向信息交互, 从车载计算机(VOBC)、自动列车监控(ATS)和计算机联锁系统(CI)以及轨道沿线的许多传感器接收信息, 由此实现为列车分配移动授权的功能.ZC系统通过与这些外部实体进行交互, 以此获取相应的位置信息, 从而完成对列车移动权限的分配.每个实体我们称为设备, 这些设备不仅包括很多物理世界中的物理实体, 例如信号机、列车、轨道、传感器等, 还包括与ZC交互的其他现有系统, 比如VOBC、ATS等, 甚至包括虚拟列车保护等的逻辑概念.这些设备组成ZC的环境E, 其中, 设备的每个状态都可以用更多的变量来表示.例如, 在轨道上有一种叫做道岔(point)的设备需要5个变量来描述:一个状态变量表示它的状态是正常、反向或未知的值之一; 另4个变量, 即nextidx_1~nextidx_4, 表示它旁边的块的ID.因此, E的形式化描述由ZC环境中的这些设备定义, 每个设备由一组变量定义.由于在有限的空间中存在太多的设备(超过1 000多个), 因此使用Di来对设备进行表示.E可以形式化地表示如下.
定义1(环境E).是所有与M交互的设备Di的集合, 而每个设备Di是变量vij的集合, 即
| $E = \{ {D_i}|1 \le i \le n\} , {D_i} = \{ {v_{ij}}|1 \le i \le n, 1 \le j \le m\} . $ |
根据发送者不同, M和E之间的相互作用可分为两组:a, c和b(遵循PF的约定).a, c中的交互是由环境E发送的现象, 而b中的交互是由机器M发送的现象.a, b和c中的交互是E中变量vij(1≤i≤n, 1≤j≤m)的函数表示:
| ${f_i}\left( {{V_{11}}, \ldots , {V_{nm}}} \right), {g_j}\left( {{V_{11}}, \ldots , {V_{nm}}} \right){\rm{和}}{h_k}\left( {{V_{11}}, \ldots , {V_{nm}}} \right). $ |
R是一组安全需求.本文中的安全需求采用文献[18]中的定义, 为机器应满足或者不违反的条件, 以确保人员安全.安全需求的一个例子是“一列火车决不能撞到另一列车”.一般来说, R通常是用自然语言编写的, 可以分解成若干个子需求.例如, 上面的例子可以分解为2个子需求:(1) ZC必须确保MA中没有另一列车; (2) VOBC必须确保列车速度不超过速度曲线.在大多数情况下, 子属性可以在领域标准中找到, 如IEEE1474.3[20].根据以上描述, 我们得到ZC的安全需求问题, 如图 1所示.
|
Fig. 1 A schematic diagram of the problem diagram in ZC 图 1 ZC问题图的示意图 |
在问题图的基础上, 定义ZC里面的情景来表示每个R的子需求是如何实现的.ZC和设备(如列车、相应传感器等)之间紧密结合, 在接收到物理实体发送的信息后, 对列车前方轨道的可运行情况进行计算, 并将计算结果返回列车, 以便对列车进行控制.以ZC的核心功能移动授权的计算与分配来举例, 在单个计算周期内, ZC需与多个设备(如列车、轨道、信号机、其他ZC等)进行交互.一般来说, 列车首先向ZC发起移动授权请求, 然后ZC接受包括列车在内的多个设备的相关信息, 根据这些信息进行移动授权的计算, 并把计算的授权终点坐标结合其他相关信息组成移动授权报告, 再发送给列车.
根据上述的描述, 可以大概描述每个R的子需求对应的情景图.在行为交互部分中, 外部设备将环境信息发送给ZC, 在对列车前方轨道的安全情况进行计算后, 将结果发送给控制设备.在期望交互的部分中, 期望外部设备将环境信息发送给ZC, ZC依据需求再从环境中获取其他有效信息, 然后控制设备的状态发生变化.在交互使能的部分中, 当外部设备将环境信息发送给ZC时, 期望交互部分中同时期望这一现象发生, 因此它们之间存在同步关系; 期望ZC从环境中感知其他有效信息从而触发接下来的行为交互, 因此存在期望使能关系; 当ZC将计算结果发送给控制设备后, 期望控制设备的状态发生改变, 因此行为交互和期望交互之间存在行为使能关系.据此, 得到ZC的子需求情景图, 如图 2所示.
|
Fig. 2 A schematic diagram of the scenario graph in ZC's sub-requirements 图 2 ZC的子需求情景图示意 |
在图 1问题图和图 2类似(假设)的n个情景图的基础上, 根据文献[19], 对问题ZC使用需求分解方法可以得到多个子需求问题, 即P={P1, …, Pn}, 其中, Pi=〈Mi, Ei, ISi, Ri〉(1≤i≤n).详情这里不再阐述.
3 区域控制器的安全需求验证 3.1 验证模型的生成本文采用SCADE来完成对区域控制器的安全需求自动验证.在自动生成Scade模型之前, 需要先生成需求的验证模型.本文把需要建模和实现的机器称为验证机器(verification machine, 简称VM).VM通过观察机器M的输入变量和输出变量, 即M和环境E的交互, 来判断机器M是否在所有可达状态上满足安全需求, 并且依此生成验证报告(verification reprot, 简称VR), 值得注意的是, VR也是一个问题域, 在问题框架方法中, 将要构建的数据存储可以建模为一种称为“设计域”的问题域类型, 由问题图中带有一条竖线的矩形表示.因此, 验证系统的环境E'由机器M、环境E、验证报告VR构成, 即E'=E∪{M}∪{VR}.
环境E'之间的交互关系如下:首先, 根据图 1, 机器M和环境E之间的交互集为a, b和c.从机器M的角度来看, a, c是输入变量, b是输出变量.验证机器VM也需要观察a, b和c来判断需求R是否得到满足.因此, 环境E和验证机器VM之间的交互a', c'在内容上和a, c相同, 验证机器VM和机器M之间的交互b'在内容上和b相同. a', b', c'和a, b, c的区别在于接收方不同.这样一来, 在需求的验证模型中就可以不包括a, b和c.而对于验证机器VM和验证报告VR之间的交互, 可以用一个布尔变量bValid和一个字符串变量cExample来表示, 分别代表验证的结果, 以及当验证失败时需要提供的反例.
综上, 需求的验证模型包含了验证机器VM、验证环境E'以及交互a', b', c'和d, 其中, VM是用来验证M的验证系统; E'是VM的运行环境, 即E, M, VR的并集, VR是该验证问题的验证报告, 包括验证结果bValid和失败时反例cExample; IS'=a'∪b'∪c'∪d是该验证问题和E'之间的交互集合, 其中, d={int2p+1=〈VM, VR, bValid〉}∪{int2p+2= 〈VM, VR, cExample〉}.由此, 可以得到需求的验证模型的静态视图, 如图 3所示.
|
Fig. 3 Static verification model of the requirements 图 3 需求的验证模型的静态视图 |
根据上述描述, 我们设计了需求验证模型的自动构造规则, 见表 1.该转换规则是根据需求问题P自动生成为需求的验证模型, 从P中读取机器M来构建验证机器VM; 根据需求的验证结果来构建验证报告VR, E'为环境E、机器M和验证报告VR的并集; 根据IS中交互来构建IS'中新的交互:交互的发送方为原来的交互发送方, 交互的接收方为验证机器VM, 交互的内容与原来的交互内容相同; 另外, 新建与验证报告之间的交互:交互的发送方为验证机器(VM), 接收方为验证报告(VR), 内容包括验证结果(bValid)和验证失败时需要提供的反例(cExample).
|
Table 1 mapping rules from requirement problem to verification model 表 1 从需求问题到需求验证模型静态视图的构造规则 |
基于静态视图, 要研究其行为交互过程, 以此构建其动态视图.根据图 2中机器M和设备E交互的情况, 其验证过程可以设计为:首先, 验证机器VM观察到外部设备发送环境信息; 然后, VM会接收到机器M发送的交互信息; 接下来, VM能够观察到外部设备发送其状态的改变情况; 最后, 根据获得的信息, VM判断需求R的满足情况, 将验证结果和验证失败时的反例发送给验证报告VR.具体过程如图 4的上半部分所示.
|
Fig. 4 Scenario graph of the verification system 图 4 验证系统的情景图 |
3.2 验证性质的生成
待验证的性质R'实际上就是要验证机器M是否满足需求R.按照问题框架的表示, 实际上就是要增加验证问题的需求、需求引用和约束.其中, 验证问题的需求就是R', 下面按E'领域来考虑需求对其现象的引用和约束.
首先, 对于环境E, 由于E与VM的交互为a', c', 与M的交互为a, b和c, 其中, a', c'来自a, c, a, c中的交互是由环境E发送的现象, 这种现象是要观察的, 因此验证需求R'要引用交互a', c'中的现象, 在R'和E之间存在需求引用a', c'.对于机器M来说, 它与VM的交互为b', 与E的交互为a, b和c, 其中, 交互b'来自于交互b, 其在内容上和b相同且由机器M发送到验证机器VM, R'要通过验证机器VM来验证机器M是否满足需求R, 因此需要引用b'.对于验证报告VR而言, 其与VM之间的交互d是VM发送给VR的需求验证结果和验证失败时的反例, R'期望验证报告的报告效果(reportEfforts)发生改变, 因此, R'和VR之间存在约束e={int2p+3=〈VR, VM, reportEfforts〉}, 因此, IS'=IS'∪e.综上, 我们在图 3的基础上, 增加R'、需求约束与需求引用, 得到验证系统的问题图来对其进行静态描述, 如图 5所示.
|
Fig. 5 Problem diagram of verification system 图 5 验证系统的问题图 |
基于验证系统的问题图, 根据图 2中需求问题的引用和约束的先后顺序关系, 设计验证系统的需求约束和约束引用的先后顺序关系, 可以得到相应的动态视图, 如图 4的下半部分所示.首先, R'期望VM能观察到外部设备发送的环境信息; 然后, VM接收到M发送的交互信息; 接下来, 期望VM能观察到外部设备发送的其状态的变化; 然后, 期望验证报告VR的报告效果发生变化.
3.3 验证的Scade实现对于一个验证问题VPi, 需要使用SCADE Suite对其进行建模并用内嵌的Design Verifier进行验证.根据Scade语言特点, 就是要设计图 5验证问题中E、M、VR和VM以及验证性质R'.这些设计中必须包含其领域特性, 这些领域特性更多包含在图 2的ZC系统的情景图中, 只有VR的性质是体现在图 4的验证系统的情景图中.因此, 本文从图 5验证系统的问题图和图 2系统的情景图出发, 设计了自动生成Scade模型的规则, 如图 6所示.
|
Fig. 6 SCADE model conversion diagram for verification problem 图 6 验证问题SCADE模型转换示意图 |
在Scade模型中, 分为两个层级:首先是顶层操作符, 主要描述问题图中不同领域之间的关系, 即M, E, VR之间的连接方式, 对应在Scade中分别为操作符M、操作符E和操作符O.操作符O, 即观察者, 被用来描述所需要验证的性质.对于该验证问题中操作符O的构建, 其实就是要判断需求的期望交互是否能发生.根据情景图对于期望交互的描述, 操作符O需要判断情景图中所有的期望交互是否被满足.值得注意的是, 在问题图中, 并没有描述交互之间的先后顺序.根据情景图以及Scade的语义模型, 可以得到如下所述的每个模块的输入输出集合:操作符M的输入为所有E发出的、M接受的变量集合, 输出为M发出的、E接受的变量集合.操作符E的输入为操作符M的输入变量集合, 并以Scade语言中断言的形式将操作符E对这些变量的影响反馈给操作符M, 即没有显示输出.在实际的建模过程中, 这部分变量往往以感应器(sensor)的方式进行定义.操作符O的输入为操作符M的输入变量和输出变量, 输出为单个布尔变量, 用来表示M是否满足R'.通过实线可以将这3个操作符进行连接.具体的设计如算法1所示.
● M根据行为交互进行设计, 也就是说, 为每个交互设计一个操作符BOi, 该操作符的输入输出由情景图中对于该交互的建模得到.同时, 不同BOi之间仅有并行关系, 而没有实体线对它们进行连接.在对BOi进行进一步的设计时, 也遵循行为交互所包含的信息, 设计其数据流模型, 完成BOi操作符的实现.具体细节见算法1的第3行~第14行.
● E根据交互使能进行设计, 首先, 根据问题图中建模的问题领域, 对每个问题领域创建一个操作符Di, 该操作符的输入由问题图中该领域相关的交互来设计; 然后, 在每个操作符Di中, 根据交互使能对其进行进一步设计.具体来说, 在问题图和情景图中, 由E发起的交互的变量, 在Scade模型中设定为感应器(sensor)类型的变量, 通过对该变量进行断言(assert), 把问题领域由交互产生的影响反馈给M.变量来自单个问题领域的断言在具体Di中进行描述; 变量来自多个问题领域的断言在E中进行描述.具体细节见算法1的第15行~第26行.
● O根据期望交互进行设计, 根据情景图中建模的期望交互, 在O中设计相对应的操作符EOi, 对每个期望交互进行设计建模.操作符EOi的输入由相对应的交互而来, 输出则是一个布尔变量, 用来表示M是否满足该期望交互.并且, 所有EOi的输出由and操作符连接, 作为O的输出变量.此外, 当存在多个R'时, 会建立多个O, 可以把这些O的输出变量通过and操作符连接, 从而同时验证多个属性.具体细节见算法1的第27行~第35行.
算法1. Scade模型生成算法.
Input:验证系统问题VP=〈VM, E', IS', R'〉;
系统情景图:Scenario=〈NodeSet, AssSet, FlowSet〉, NodeSet=〈BehSet, ExpSet〉.
Output:Scade模型N={operators}.
1: Begin;
2: N=NULL;
3: 构建验证系统操作符DV, N=N∪{DV}:
4: for问题图和情景图中所有交互变量Variable
5: DV.input={int|int∈NodeSet}∪DV.input; //DV的输入变量为问题图和情景图中所有交互变量
6: DV.output={BooleanVariable}; //DV的输出变量为一个布尔变量, 用来表示M是否满足R'
7: 构建操作符M, N=N∪{M};
8: M.input={variable|int=〈*, M, variable〉, int∈BehSet}; //M的输入为所有行为交互中M接受的交互变量集合
9: M.output={variable|int=〈M, *, variable〉, int∈BehSet}; //M的输出变量为所有行为交互中M发出的交互变量集合
10:for (each BehEnai or ReqEnai∈NodeSet)
11: 构建操作符BOi in M;
12: BOi.input为该使能中所涉及到的交互变量集合;
13: BOi.output的输出为该使能所需要发出的交互变量集合;
14:Endfor
15 构建操作符E, N=N∪{E}
16: 定义E的输入变量集合:所有交互使能中涉及到的交互变量集合;
17: 定义E的输出变量集合:无;
18:for (each domain∈E') //构建操作符E中的Di
19: 构建操作符Di, E=E∪Di
20: for (each Ass∈AssSet)
21: if (Ass的变量来自单个Di)
22: 在Di中创建表达式或操作符, 描述Ass;
23: else在E中创建表达式或操作符, 描述Ass;
24: endif
25: endfor
26:endfor
27:构建操作符O, N=N∪{O};
28:定义O的输入变量集合:M, E的输入变量集合和输出变量集合的并集
29:定义O的输出变量集合:一个布尔型变量Result;
30:for (each expBeh∈ExpSet)
31: 在O中根据期望使能构建操作符EOi, O=O∪EOi
32: EOi的输入为{variable|int=〈*, *, variable〉}
33: EOi的输出为布尔变量Result
34:endfor
35:把所有EOi的输出变量用AND操作符连接, 并连至O的输出变量Result;
36:把M, E, O拖入DV中;
37:连接DV的输入变量至M, E, O的输入变量;
38:连接M的输出变量至E的输入变量;
39:连接O的输出变量至DV的输出变量;
40:End;
4 案例研究本节用ZC的核心子系统CAL_EOA作为案例.限于篇幅, 我们将案例做了一定的简化.CAL_EOA负责计算并分配移动授权.移动授权(movement authority, 简称MA)指的是轨旁设备分配给列车对于该区域的行驶许可, 即告诉车辆前方的轨道在多大程度上能够安全运行.计算过程如下:随着列车的移动, 列车必须和轨旁设备保持连续的通信; 在通信过程中, 列车的位置信息和刹车曲线也在被连续地计算, 并从列车发送到轨旁设备.根据这些信息, 轨旁设备能够建立保护区域, 确保其他列车不会进入.这个区域被称为移动授权区域.这个区域的终点被称为授权终点(end of authority, 简称EOA), 列车在一个移动授权中被允许行驶到该点, 但速度必须降为0.
4.1 需求的建模和分解CAL_EOA就是我们要开发的软件, 它涉及到如下设备:列车(train, 简称TR)、区块(block, 简称BL)、分支(branch, 简称BR)、区块布局(block layout, 简称LO)、分支布局(branch layout, 简称RO)、其他列车(other train, 简称OT)、信号机(signal, 简称SI)、区域控制器边界(ZC boundary, 简称ZB)、行驶方向(traffic direction, 简称TD)、缓冲区(buffer zone, 简称BZ)、重叠区(overlap, 简称OL)等.这些设备共同构成了CAL_EOA的环境, 即
| $E = \left\{ {TR, BL, BR, LO, RO, OT, SI, ZB, TD, BZ, OL} \right\}. $ |
在需求R方面, IEEE标准1474.3的第6.3节中提到移动保护的限制和目标点确认(limit of movement protection and target point determination)[20].根据该节内容及相关文档(如IEEE标准1474.1[8]的第6.1.2节), 可以得到一条SIL-4安全级别(即最高安全级别)的功能需求RCAL_EOA:CAL_EOA需要为注册在当前区域控制器下的列车计算移动授权终点, 并将其发送给相应列车.根据移动授权不同的情况, 可以分为8个子需求, 见表 2.
|
|
Table 2 List of safety sub-requirements in CAL_EOA 表 2 CAL_EOA中的安全子需求列表CAL_EOA中的安全子需求列表 |
对于需求R1, CAL_EOA从Train、Block、Branch、Block Layout和Branch Layout中分别读取列车定位信息、Block逻辑分布、Branch逻辑分布、Block实体分布以及Branch实体分布, 然后从最近的Block开始, 一个Block一个Block地寻找是否存在轨道尽头, 如果找到, 作为EOA发送.
类似地, 需求R2~R8中, 也都是从不同的设备集合中读取列车定位信息、Block逻辑分布、Branch逻辑分布等信息, 从最近的Block开始, 一个Block一个Block地寻找是否存在其他列车(R2)、是否存在非受控道岔(R3)、是否存在区域控制器边界(R4)、是否存在非连续TD(R5)、是否存在缓冲区(R6)、是否存在断链点(R7)、是否存在重叠区(R8), 如果找到, 作为EOA发送.
从上述描述中, 我们可以得到交互集合IS, IS={int1, int2, …, int48}, 其中, {int1, …, int9}为Train发送给CAL_EOA的列车定位信息, {int10, int11}为CAL_EOA发送给列车的EOA报文, {int12, …, int15}为Block发送给CAL_EOA的BLOCK逻辑分布, {int16, …, int18}为Branch发送给CAL_EOA的Branch逻辑分布, {int19, …, int22}为Block Layout发送给CAL_EOA的Block实体分布, {int23, …, int25}为Branch Layout发送给CAL_EOA的Branch实体分布, {int26, …, int34}为Other Train发送给CAL_EOA的其他列车定位信息, {int35, …, int37}为Signal发送给CAL_ EOA的信号机位置和状态, {int38, int39}为ZC boundary发送给CAL_EOA的区域控制器边界信息, {int40, …, int42}为Traffic Direction发送给CAL_EOA的Block的可行驶方向信息, {int43, …, int45}为Buffer Zone发送给CAL_ EOA的SI后的缓冲区信息, {int46, int47}为Overlap发送给CAL_EOA的重叠区信息, int48为Train发送给CAL_ EOA的报文接受状态.上述交互inti(1≤i≤48)的定义及变量的含义具体见表 3.
|
|
Table 3 Interactive list of problem diagrams for CAL_EOA and its validation model 表 3 CAL_EOA及其验证模型的问题图的交互列表 |
根据上述信息, 可以得到CAL_EOA的问题图, 如图 7所示.
|
Fig. 7 Problem diagram of CAL_EOA 图 7 CAL_EOA的问题图 |
接下来, 对每个子需求绘制情景图.以R1为例, 在行为交互部分中, Train、Block、Branch、Block Layout和Branch Layout分别向CAL_EOA发送列车定位信息(int1, …, int9)、Block逻辑分布(int12, …, int15)、Branch逻辑分布(int16, …, int18)、Block实体分布(int19, …, int22)以及Branch实体分布(int23, …, int25), 在接收到信息之后, CAL_ EOA将移动授权终点的计算结果发送给列车(int10, int11).在期望交互部分中, Train、Block、Branch、Block Layout和Branch Layout分别向CAL_EOA发送列车定位信息(int1, …, int9)、Block逻辑分布(int12, …, int15)、Branch逻辑分布(int16, …, int18)、Block实体分布(int19, …, int22)以及Branch实体分布(int23, …, int25), 然后期望列车的消息状态变为Received(int48).在交互使能部分中, 由于行为交互和期望交互都需要获取Train、Block、Branch、Block Layout和Branch Layout向CAL_EOA发送的信息, 因此它们之间存在同步关系; 当列车接收到CAL_EOA发送的结果报告后, 消息接收状态变为Received, 因此, int11和int48之间存在行为使能关系.
最终, 得到一个情景图, 如图 8所示.
|
Fig. 8 Scenario graph of R1 图 8 R1的情景图 |
类似地, 可以得到其他的7个子需求的情景图, 限于篇幅, 详见网址https://github.com/lxsbamboo/ZC- Verification.git.基于根据这些情景图, 使用文献[19]中的基于情景的需求投影方法, 将问题图 5分解, 得到8个子问题.每个子问题都对应解决一个子需求, 有自己的子环境和子交互.这8个问题是类似的.以子问题P1为例, 其用来对子需求R1进行验证, 在待开发软件中, P1涉及到的子机器为M1, 和M1进行交互的外部实体为子环境E1, 包括Train、Block、Branch、Block Layout和Branch Layout, IS1为M1和E1之间发生的交互, 其中, {int1, …, int9}为Train发送给M1的列车定位信息, {int12, …, int15}为Block发送给M1的Block逻辑分布, {int16, …, int18}为Branch发送给M1的Branch逻辑分布, {int19, …, int22}为Block Layout发送给M1的Block实体分布, {int23, …, int25}为Branch Layout发送给M1的Branch实体分布, {int10, int11}为M1经过计算后发送的EOA报文, int48为Train的报文接收状态.其他子问题详见表 4.
|
|
Table 4 Decomposition results of sub-problem diagrams 表 4 子问题图的分解结果 |
4.2 需求验证模型的生成
根据表 1中的转换规则, 可以根据每个子问题的问题图自动生成其对应的需求验证模型.以子问题P1为例, 说明其具体的生成过程.首先, 根据子机器M1构建的验证子机器可以构造VM1.VR1为验证报告.E1, M1和VR1共同构成验证子问题的环境E'1, 接下来生成VM1和E'1之间的交互.
对于M1和E1之间的交互a, b, c, d, e, f, m而言, 由于其交互发送方及交互内容不变, 交互的接收方变为验证子机器VM1, 因此用a', b', c', d', e', f', m'来表示VP1中VM1与E1和M1之间的交互, 并且构成新的验证子交互IS'1, 其中, {int49, …, int57}为Train发送给VM1的列车定位信息、{int58, int59}为CAL_EOA发送给VM1的EOA报文、{int60, …, int63}为Block发送给VM1的Block逻辑分布、{int64, …, int66}为Branch发送给VM1的Branch逻辑分布、{int67, …, int70}为Block Layout发送给VM1的Block实体分布, {int71, …, int73}为Branch Layout发送给VM1的Branch实体分布, int96为Train的报文接收状态.n表示VM1与验证报告VR1之间的交互, 其中int97表示VM1发送给VR1的验证结果bVlid, int98为VM1发送给VR1的验证错误时反例, int99为VR1发送给VM1的报告效果
reportEfforts.因此, $I{S'_1} = I{S'_1} \cup \{ in{t_{97}}, in{t_{98}}, in{t_{99}}\}$.
根据图 8中的交互情况, 我们可以得到需求验证模型的动态视图.首先, VM观察到Train、Block、Branch、Block Layout和Branch Layout分别发送列车定位信息(int49, …, int57)、Block逻辑分布(int60, …, int63)、Branch逻辑分布(int64, …, int66)、Block实体分布(int67, …, int70)以及Branch实体分布(int71, …, int73); 然后, VM接收到CAL_EOA发送的移动授权终点的计算结果(int58, int59); 接下来, VM观察到列车发送的报文接收状态(int96); 最后, 根据获得的信息, VM将CAL_EOA是否满足需求R1的验证结果(int97)和验证错误时的反例(int98)发送给验证报告VR.限于篇幅, 具体的视图参见https://github.com/lxsbamboo/ZC-Verification.git.
4.3 需求验证性质的生成同样以子问题P1为例, 可以根据子问题图中的需求R自动生成验证性质R'.R'引用机器M1和环境E1发送给VM的交互a', b', c', d', e', f', m', 并约束VM和VR间的交互o.由上述描述, 子问题P1生成的验证系统的问题图VP1可以对其进行静态描述, 如图 9所示.机器M1和环境E1发送交互信息给验证机器VM, 然后, VM对机器M1是否满足需求R进行验证并向VR发送验证结果和错误时的反例.通过问题领域M1和E1中的交互和期望生成的VM和VR间的交互来判断是否满足验证性质R'.其中, 交互的具体定义及变量的含义见表 3.
|
Fig. 9 A problem diagram for verifying sub-problem VP1 图 9 验证子问题VP1的问题图 |
基于图 9验证子问题VP1的问题图, 根据图 8中需求引用和约束的先后顺序关系, 我们可以对子问题R1的验证系统进行动态的描述:首先, VM观察到Train、Block、Branch、Block Layout和Branch Layout分别发送的列车定位信息(int49, …, int57)、Block逻辑分布(int60, …, int63)、Branch逻辑分布(int64, …, int66)、Block实体分布(int67, …, int70)以及Branch实体分布(int71, …, int73); 然后, CAL_EOA将移动授权终点的计算结果发送给VM(int58, int59); 接下来, VM观察到列车发送的报文接收状态(int96); 最后, 期望VR的报告效果reportEfforts发生变化(int99).限于篇幅, 具体过程参见https://github.com/lxsbamboo/ZC-Verification.git.
4.4 需求验证问题Scade模型的生成基于8个验证子问题图以及子问题的情景图, 根据算法1, 可以自动生成8个Scade模型, 对其进行组合即可对安全需求进行验证.还是以VP1为例, 说明其Scade模型的生成.操作符M用来描述行为交互, 它的输入变量为行为交互中所有M1接收的交互变量的集合, 也就是E1发送给M1的设备位置信息, 即ThaPo, THiPo等; 其输出为行为交互中所有由M1发出的交互变量集合, 也就是M1发送给的移动授权分配结果, 即EOAPos和EOATyp.操作符E用来描述交互使能, 在图 8中, {int1, …, int9, int12, …, int25}之间存在同步序关系, int11和int48之间存在行为使能关系, 因此, E的输入{int1, …, int9, int11, …, int25, int48}中的交互变量.在操作符E中, E1发送的设备位置信息用局部变量来表示, EOA报文和报文接收状态receives用传感器表示, 在E中创建断言来表示这些交互之间的使能关系.操作符O用期望交互描述, 其输入为M和E的所有输入和输出变量集合的并集, 输出为验证结果Result.图 10是该验证子问题的Scade模型示意图, 其中, 我们把局部输入变量复制了3份来提高模型的易读性.
|
Fig. 10 Scade model for verifying sub-problem VP1 图 10 验证子问题VP1的Scade模型 |
O是对期望交互的描述, 用来表示外部设备在发送相应位置信息后得到的状态变化.因此, 我们根据情景图中的期望交互来构建具体的操作符O.在操作符O中, 用局部变量来表示外部设备发送的设备位置信息, 用sensor来表示报文接收状态received.当列车位置信息(THaPo, THiPi, TTaPo, TTiPo, VHaPo, VTaPo, VTiPo, TRlen)、Block逻辑布局(BLpID, BLnID, BLLen, BLiBR)、Branch逻辑布局(BRpID, BRnID, BRLen)、Block实体布局(LOpID, LOnID, LOLenLOiBR)和Branch实体布局(ROpID, ROnID, ROLen)全部发送成功, 即以上变量皆不为空时, 我们希望Train的报文接收状态变为received, 即received变量不为空.对以上结果用imply操作符连接, 并将判断结果输出.根据以上描述, 我们可以得到操作符O的具体内容, 如图 11所示.
|
Fig. 11 Operator O in the Scade model 图 11 Scade模型中的操作符O |
类似地, 我们得到所有的8个验证子问题的SCADE模型.这8个子问题类似.在现实规模上, 以VP1为例, 它有19个设备, 包括3辆车(train)、6个区块(block)、6个分支(branch), 其他设备各1个.它与这些设备的交互大约有265个变量现象.在进行验证时, 使用如下机器配置:WIN7操作系统, 处理器为E5 2620 v3, RAM为64GB, 可以得到ZC的8个安全子需求皆能验证成功, 其中, 子问题7的验证时间最短, 131s;子问题4的验证时间最长, 为147s.每个子问题验证的平均时间为138s, 所有子问题的总验证时长为1 103s.所有子问题的验证结果详见网址https://github.com/lxsbamboo/ZC-Verification.git.实际上, 之前由于CAL_EOA问题过大, 验证过程中出现了状态爆炸问题, SCADE中的内置验证器无法对该系统进行验证.对比之下, 充分说明必须对模型进行分解, 最好能够在需求阶段进行分解.
5 相关工作本文研究轨道交通系统的安全需求的自动验证问题.已经有很多安全需求的验证工作.根据安全需求的描述方式不同, 可以分为半形式化需求的验证和形式化需求的验证.
半形式化需求的验证, 实际上是指需求是由基于统一建模语言(UML)[21]等半形式化语言表示, 可以由领域专家绘制, 而验证则要将半形式化语言转换为形式化语言进行.这方面的工作也很多, 例如, 黄友能等人[12]采用扩展后的UML对ZC子系统的系统功能进行半形式化建模, 然后根据转换规则将UML模型转换为线性混成自动机的形式化模型, 使用BACH软件[22]进行验证, 验证的是需求的一致性; Fotso等人[13]使用SysML/KAOS[23]对系统需求、领域特性以及与混合ERTMS/ETCS 3级标准[24, 25]相关的安全不变量进行半形式化建模, 然后自动转换为B系统[26]规范, 以获得形式化规范的体系结构, 最后用Rodin工具[27]对其进行验证, 也是验证的需求的一致性; 杨璐等人[14]采用半形式化方法消息顺序图(message sequence chart, 简称MSC)[28]对ZC切换场景功能和受限活性, 然后将MSC模型转换为形式化的时间自动机, 通过UPPAAL[29]对其进行验证.我们的方法本质上也是属于这种类方法, 但本文的优点在于:(1)问题框架方法在建模需求时其独特的环境视角与其他的建模语言有本质的区别, 它更适合建模ZC这类系统; (2)自动的需求分解, 可以极大地降低系统复杂度; (3)自动的验证模型生成, 非常方便领域专家使用; (4)与其他需求一致性验证不同, 本文验证的是规约是否满足需求, 属于需求可满足性验证的一种; (5)基于需求分解的组合验证, 可以提高验证效率, 部分缓解因复杂带来的状态空间爆炸.
在形式化需求验证中, 都是形式化专家根据领域专家的自然语言描述, 直接建立形式化模型, 并采用相应的形式化验证工具进行性质验证.例如, Hartig等人[9]在对用自然语言描述的铁道车辆的安全需求进行分析之后, 使用ANSI/ISO-C规范语言(ACSL)[30]将其形式化, 然后通过FRAMA-C[31]对形式化模型进行演绎验证; 李蓉[10]使用SCADE来对用自然语言描述的ZC系统功能进行形式化建模与验证; Aiello等人[32]形式化需求建模语言(Form-L)[33]对使用自然语言描述的飞机子系统部件及其设计变体的需求进行建模, 通过Modelica需求库[34, 35]将需求的Form-L模型映射到Modelica[36]上, 通过仿真实现对需求的验证; Chhabra等人[11]构建了一个基于Petri网和域的上下文推理的工具, 将自然语言规范转换为形式化的表示决策表(expressive decision table, 简称EDT)[37], 然后使用转换过程中的本体来验证给定的其他需求, 以检查它们与现有需求的一致性.上述验证方法, 对于不具有形式化知识的领域专家来讲很难使用.而本文提出的方法是使用PF进行需求的建模, 使用的原语为现实中的实体和实体与待构建的软件之间的交互, 领域专家对此十分熟悉, 相比来说会方便使用很多.另外, 本文方法可以自动地去验证, 不仅如此, 我们还是一种组合验证方法, 可以验证复杂的系统, 特别适合ZC这类系统.
6 结束语ZC是一个复杂的安全攸关系统, 其安全需求的可满足性需要形式化的验证.本文提出了ZC系统安全需求建模、分解与自动验证的方法, 采用PF方法对ZC的安全需求问题进行建模, 继而通过基于情景的自动分解方法将需求问题分解成较小的子问题, 根据每个子问题的需求模型自动生成需求的验证子问题模型, 然后自动生成验证子问题的Scade形式化模型, 最后通过模型检验器Design Verifier对Scade模型进行了验证.本文的主要贡献为设计了一个基于问题框架模型的ZC系统的安全需求自动验证方法, 根据需求模型自动生成安全需求验证问题模型和验证性质, 并生成由Scade语言描述的验证模型, 进行组合验证.通过该方法可以由半形式化需求模型自动生成形式化模型进行验证, 降低了ZC验证的难度, 使得领域专家也可以做形式化验证.
我们将该方法应用到实际的轨道交通区域控制器的安全需求的建模、分解与验证中, 并做了一些实验.实验结果证明, 使用该方法可以有效地缓解状态空间爆炸问题, 并能实现对安全需求自动验证, 且验证时间成本大为降低, 这使得ZC的安全需求验证问题有了明显的进步.本方法不仅为轨道交通系统, 也为其他类似复杂系统, 如信息物理系统的需求验证提供了一个很好的借鉴思路.
| [1] |
Gao CH. Research on the key techniques of the independent and innovative CBTC. Urban Rapid Rail Transit, 2011, 24(4): 1-4(in Chinese with English abstract).
[doi:10.3969/j.issn.1672-6073.2011.04.001] |
| [2] |
Lutz RR. Analyzing software errors in safety-critical embedded systems. In: Proc. of the IEEE Int'l Symp. on Requirements Engineering. San Diego: Computer Society, 1993, 126-133.
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=CC025637437 |
| [3] |
McDermid JA. Software safety: Where's the evidence? In: Proc. of the 6th Australian Workshop on Safety Critical Systems and Software, Vol.3. St Lucia: Australian Computer Society, 2001, 1-6.
http://d.old.wanfangdata.com.cn/OAPaper/oai_doaj-articles_77ad244a290c7b0181a6f19601d19ffe |
| [4] |
Barnat J, Bauch P, Benes N, Brim L, Beran J, Kratochvila T. Analysing sanity of requirements for avionics systems. Formal Aspects of Computing, 2016, 28(1): 45-63.
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=3f752ee18b63ddad049ab8e16e43d287 |
| [5] |
BS EN 50128. Railway Applications—Communication, Signaling and Processing Systems—Software for Railway Control and Protection Systems. British Standards Institute, 2011.
|
| [6] |
BS EN 50129. Railway Application—Communications, Signaling and Processing Systems—Safety Related Electronic Systems for Signaling. British Standards Institute, 2018.
|
| [7] |
Yang XW. Modeling and safety verification of zone controller in CBTC with UML [MS. Thesis]. Beijing: Beijing Jiaotong University, 2008(in Chinese with English abstract).
|
| [8] |
Yuan Z, Chen X, Liu J, Yu Y, Sun H, Zhou T, Jin Z. IEEE Std 1474.1-2004 IEEE Standard for Communications-based Train Control (CBTC) Performance and Functional Requirements. The Rail Transit Vehicle Interface Standards Committee, 2005.
https://standards.ieee.org/standard/1474_1-2004.html |
| [9] |
Hartig K, Gerlach J, Soto J, Busse J. Formal specification and automated verification of safety-critical requirements of a railway vehicle with Frama-C/Jessie. In: Proc. of the FORMS/FORMAT 2010. Berlin, Heidelberg: Springer-Verlag, 2011, 145-153.
http://cn.bing.com/academic/profile?id=004531cdd8391d7c0f00826159fcbe5b&encoded=0&v=paper_preview&mkt=zh-cn |
| [10] |
Li R. Modeling and verification of zone controller in CBTC with SCADE [MS. Thesis]. Chengdu: Southwest Jiaotong University, 2015(in Chinese with English abstract).
|
| [11] |
Chhabra A, Sangroya A, Anantaram C. Formalizing and verifying natural language system requirements using Petri nets and context based reasoning. In: Proc. of the MRC@ IJCAI. Stockholm: CEUR-WS.org, 2018, 64-71.
http://cn.bing.com/academic/profile?id=ac347be068622c8b44aaced912bfd313&encoded=0&v=paper_preview&mkt=zh-cn |
| [12] |
Huang YN, Zhang PJ, Hou XP, Tang T. Modeling and verification method of ZC subsystem in urban rail transit based on hybrid automata. China Railway Science, 2016, 37(2): 114-121(in Chinese with English abstract).
[doi:10.3969/j.issn.1001-4632.2016.02.16] |
| [13] |
Fotso SJT, Frappier M, Laleau R, Mammar A. Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. In: Butler MJ, ed. Proc. of the Int'l Conf. on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Southampton: Springer-Verlag, 2018, 262-276.
http://cn.bing.com/academic/profile?id=6f14acef48b0688c07167b7ec39b38e0&encoded=0&v=paper_preview&mkt=zh-cn |
| [14] |
Yang L, Chen YG. Modeling and verification of switch scene of zone controller based on MSC and UPPAAL. Railway Standard Design, 2018, 62(5): 171-174, 179(in Chinese with English abstract).
http://d.old.wanfangdata.com.cn/Periodical/tdbzsj201805036 |
| [15] |
Jackson M. Software Requirements and Specifications: A Lexicon of Practice, Principles and Prejudices. Addison-Wesley, 1995.
|
| [16] |
Jackson M. Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley, 2001.
|
| [17] |
Le Sergent T. SCADE: A comprehensive framework for critical system and software engineering. In: Proc. of the Int'l SDL Forum. Berlin, Heidelberg: Springer-Verlag, 2011, 2-3.
http://d.old.wanfangdata.com.cn/Periodical/ckjs201112018 |
| [18] |
Yuan Z, Chen X, Liu J, Yu Y, Sun H, Zhou T, Zhi J. Simplifying the formal verification of safety requirements in zone controllers through problem frames and constraint-based projection. IEEE Trans. on Intelligent Transportation Systems, 2018, 19(11): 3517-3528.
[doi:10.1109/TITS.2018.2869633] |
| [19] |
Jin Z, Chen X, Didar Z. Performing projection in problem frames using scenarios. In: Sulaiman S, ed. Proc. of the 2009 16th Asia- Pacific Software Engineering Conf. Batu Ferringhi: IEEE Computer Society, 2009, 249-256.
http://cn.bing.com/academic/profile?id=975e80780f75108014a715aba52d3c37&encoded=0&v=paper_preview&mkt=zh-cn |
| [20] |
IEEE Recommended Practice for Communications-based Train Control (CBTC) System Design and Functional Allocations. IEEE Standard 1474.3-2008, 2008. 1-117.
|
| [21] |
Fowler M, Kobryn C. UML Distilled: A Brief Guide to the Standard Object Modeling Language. Addison-Wesley Professional, 2004.
|
| [22] |
Bu L, Li Y, Wang L, Li X. BACH: Bounded reachability checker for linear hybrid automata. In: Cimatti A, ed. Proc. of the 2008 Formal Methods in Computer-aided Design. Portland: IEEE, 2008, 1-4.
http://d.old.wanfangdata.com.cn/Periodical/rjxb201104004 |
| [23] |
Gnaho C, Semmak F. Une extension SysML pour l'ingénierie des exigences dirigée par les buts. In: Proc. of the INFORSID., 2010, 277-292.
http://d.old.wanfangdata.com.cn/NSTLQK/NSTL_QKJJ0223872008/ |
| [24] |
EEIG ERTMS Users Group. Hybrid ERTMS/ETCS Level 3. Principles Ref: 16E042, Version 1A, 2017.
|
| [25] |
Furness N, van Houten H, Arenas L, Bartholomeus M. ERTMS Level 3: The game-changer. IRSE News, 2017, 232: 2-9.
|
| [26] |
Abrial JR. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
|
| [27] |
Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L. Rodin: An open toolset for modelling and reasoning in Event-B. Int'l Journal on Software Tools for Technology Transfer, 2010, 12(6): 447-466.
[doi:10.1007/s10009-010-0145-y] |
| [28] |
Rudolph E, Graubmann P, Grabowski J. Tutorial on message sequence charts. Computer Networks and ISDN Systems, 1996, 28(12): 1629-1641.
[doi:10.1016/0169-7552(95)00122-0] |
| [29] |
Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W. UPPAAL—A tool suite for automatic verification of real-time systems. In: Proc. of the Int'l Hybrid Systems Workshop. Berlin, Heidelberg: Springer-Verlag, 1995, 232-243.
[doi:10.1007/BFb0020949] |
| [30] |
Baudin P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V. ACSL: ANSI/ISO C specification language. Version 1.4. 2009. http://framac.cea.fr/download/acsl_1.4.pdf
|
| [31] |
Correnson L, Cuoq P, Puccetti A, Signoles J. Frama-C user manual, boron release. 2010. http://frama-c.com/download/user-manual-Boron-20100401.pdf
|
| [32] |
Aiello F, Garro A, Lemmens Y, Dutré S. Formal modeling of system properties for simulation-based verification of requirements: Lessons learned. In: Fierro D, ed. Proc. of the 3rd INCOSE Italia Conf. on Systems Engineering. Naples: CEUR-WS.org, 2017, 54-61.
http://cn.bing.com/academic/profile?id=09b0fc82f5e6de5eee2e3aa2180aa6e2&encoded=0&v=paper_preview&mkt=zh-cn |
| [33] |
Nguyen T. FORM-L: A modelica extension for properties modelling illustrated on a practical example. In: Proc. of the 10th Int'l Modelica Conf., Vol.96. Lund: Linköping University Electronic Press, 2014, 1227-1236.
http://cn.bing.com/academic/profile?id=57d3f6b6125eff5f6a20ca6294e6a9a2&encoded=0&v=paper_preview&mkt=zh-cn |
| [34] |
Garro A, Tundis A, Bouskela D, Jardin A, Thuy N, Otter M, Buffoni L, Fritzson P, Sjölund M, Schamai W, Olsson H. On formal cyber physical system properties modeling: A new temporal logic language and a modelica-based solution. In: Proc. of the 2016 IEEE Int'l Symp. on Systems Engineering (ISSE). IEEE, 2016, 1-8.
http://cn.bing.com/academic/profile?id=8adef7c6b8c37c1a33368a180c5a2505&encoded=0&v=paper_preview&mkt=zh-cn |
| [35] |
Otter M, Thuy N, Bouskela D, Buffoni L, Elmqvist H, Fritzson P, Garro A, Jardin A, Olsson H, Payelleville M, Schamai W, Thomas E, Tundis A. Formal requirements modeling for simulation-based verification. In: Proc. of the 11th Int'l Modelica Conf., Vol.118. Versailles: Linköping University Electronic Press, 2015, 625-635.
http://cn.bing.com/academic/profile?id=414847c4121ec509d0b5805bc0969b51&encoded=0&v=paper_preview&mkt=zh-cn |
| [36] |
Fritzson P, Engelson V. Modelica—A unified object-oriented language for system modeling and simulation. In: Proc. of the European Conf. on Object-oriented Programming. Berlin, Heidelberg: Springer-Verlag, 1998, 67-90.
https://www.sciencedirect.com/science/article/pii/S1364815299000158 |
| [37] |
Venkatesh R, Shrotri U, Krishna GM, Agrawal S. EDT: A specification notation for reactive systems. In: Fettweis GP, ed. Proc. of the 2014 Design, Automation & Test in Europe Conf. & Exhibition (DATE). Dresden: European Design and Automation Association, 2014, 1-6.
http://d.old.wanfangdata.com.cn/NSTLQK/NSTL_QKJJ0211574183/ |
| [1] |
郜春海. 自主创新CBTC系统的核心技术研究. 都市快轨交通, 2011, 24(4): 1-4.
[doi:10.3969/j.issn.1672-6073.2011.04.001] |
| [7] |
杨旭文.基于UML的CBTC系统区域控制器的建模与安全性验证[硕士学位论文].北京: 北京交通大学, 2008.
|
| [10] |
李容.基于SCADE的CBTC区域控制器建模与验证[硕士学位论文].成都: 西南交通大学, 2015.
|
| [12] |
黄友能, 张鹏基, 侯晓鹏, 唐涛. 基于混成自动机的城市轨道交通ZC子系统建模与验证方法. 中国铁道科学, 2016, 37(2): 114-121.
[doi:10.3969/j.issn.1001-4632.2016.02.16] |
| [14] |
杨璐, 陈永刚. 基于MSC与UPPAAL的区域控制器切换场景建模与验证. 铁道标准设计, 2018, 62(5): 171-174, 179.
http://d.old.wanfangdata.com.cn/Periodical/tdbzsj201805036 |