基于STAMP与模型检验的全自动无人驾驶复杂运营场景安全验证方法

马牧云，张亚东，2，李 耀，郭 进，2

(1.西南交通大学信息科学与技术学院,成都 611756; 2.四川省列车运行控制技术工程研究中心,成都 611756;3.成都信息工程大学软件工程学院,成都 610225)

引言

近年来,随着城市人口数量不断攀升,交通运输的压力也随之增大,轨道交通能够有效改善城市发展中的交通拥堵、污染等问题,得到了飞速发展。全自动无人驾驶系统作为智慧城市轨道交通的核心技术装备之一,由于其较高的自动化程度和智能化水平而得到了广泛发展与应用[1-2]。与传统轨道交通控制系统相比,全自动无人驾驶系统能够提高行车效率,减少或取消人工操作,系统运营场景涵盖了列车自动唤醒、自动正线运营、进站停车、自动折返以及故障情况下自动恢复等数十个正常运营场景和异常场景[3]。不同运营场景下,全自动无人驾驶系统具有不同的交互主体、交互行为和控制逻辑,系统危险及致因具有较强的隐蔽性和复杂性,给运营安全带来了新的挑战。如何验证全自动无人驾驶复杂运营场景下的系统安全性,已经成为全自动无人驾驶技术迫切需要解决的关键问题之一。

传统的安全分析方法主要是基于线性事件链的系统安全理论和方法[4-5]。但随着计算机、通信等技术与安全苛求系统的不断融合,系统的复杂度和耦合度急剧上升,系统危险形式与危险致因场景呈现出更加多样化、隐蔽性与复杂化等特点,安全验证的难度骤然增大。系统事故的发生不再由单一的或几个危险事件线性叠加的结果来决定,因此,基于线性事件链的传统安全分析方法表现出了一定的局限性。为应对此类问题,2004年,Nancy Leveson提出了STAMP理论[6]。将系统视为一种分层控制结构,将安全问题转换为控制问题。之后基于STAMP理论,Leveson进一步提出STPA(System Theoretic Process Analysis)方法用于危险致因分析,这种方法采用自上而下的分析手段,能够更加系统地进行危险分析,更全面地辨识出所有会使系统进入危险状态的致因因素[7-8]。STAMP理论在系统安全领域得到了广泛发展和应用。文献[9]以列车进站停车以及站台发车异常运营场景为例,研究应用STAMP理论与STPA方法,对潜在的不安全控制行为及危险致因进行了辨识。然而,由于STAMP模型采用自然语言,缺乏形式化手段,存在模糊或歧义的问题且模型无法自动验证。针对以上问题,文献[10]结合时间自动机,探索了STPA-UPPAAL的转换规则以及分析规范,通过时间自动机模型,验证了系统的不安全控制行为,提高了不安全控制行为的验证效率。文献[11]结合有色Petri网,利用CPN模型对系统进行形式化建模,避免了自然语言的二义性,以高铁列控为例,进行了形式化验证。与以上建模方法相比,安全状态机作为图形化的同步建模语言,模型清晰、简洁,具有良好的可读性,能够用严格的语义避免需求描述的模糊性和二义性等缺陷。同时,高安全性应用开发环境SCADE[12],支持安全状态机的建模、仿真及验证。目前SCADE工具和安全状态机已在车站计算机联锁系统、列控系统等安全苛求系统的软件建模与验证方面具有了良好的应用基础。

本文基于STAMP系统安全分析理论,引入安全状态机建模方法,提出了一种基于STAMP理论与模型检验相结合的复杂运营场景安全验证方法。

1 安全分析及验证理论基础

1.1 STAMP理论与STPA方法

STAMP理论是基于系统理论和控制理论的事故致因模型。其中重要的3个要素是:安全约束、分层安全控制结构和过程模型,安全约束作为3个要素中最基本的概念,需要被正确有效地执行[13]。在构建分层控制结构模型的过程中,充分考虑组织管理,系统交互等对系统安全的影响。根据系统理论,高层次结构部分的操作复杂性由低层次结构的操作决定。高层次的约束就是对低层次的控制。在STAMP理论的基础上,Leveson提出的STPA主动分析方法用于危险致因分析,通过分析开发过程中潜在的危险致因因素,达到消除或控制危险源的目的。这种方法将分析过程主要分为以下几个步骤:分析系统级危险、构建分层控制结构模型、辨识不安全控制行为、分析危险致因因素、制定相应的安全约束[14]。在STPA方法中,实施不安全的控制行为会导致系统进入危险状态。在识别不安全控制行为时,常用的有以下4种分类[15]:

(1)未提供控制行为导致危险;

(2)提供错误的控制行为导致危险;

(3)提供控制行为的时间过早或过晚导致危险;

(4)控制行为作用的时间过长或过短导致危险。

1.2 安全状态机建模与模型检验方法

安全状态机(SSM)是一种图形化的建模语言,具有并发性、层次性和通信机制[16]。主要由状态和迁移两部分组成,有激活和未激活两种状态。迁移有两种属性,分别为条件和行为(也就是赋值语句),位于迁移线上的行为只在迁移触发时执行。位于状态机内部的行为,需要在该状态激活的每一个周期执行。状态机要从当前状态迁移至下一个状态,需要同时满足3个条件,一是当前状态处于激活态,二是满足迁移条件,三是需要满足迁移的优先级。一个操作符可以包含一个或多个状态机,状态机之间可以是并行或者嵌套的关系。如图1所示,该模型有两个状态,其中加粗边框为初始状态,如果在满足迁移条件ON=true的情况下,状态迁移触发,从START状态迁移至END状态。迁移发生的顺序根据迁移线设置的强迁移、弱迁移、同步迁移以及层次结构和优先级而有所不同。安全状态机模型可以在仿真界面通过修改迁移条件的值进行单步仿真,初步解决模型的设计问题。

图1 基础安全状态机模型

安全状态机的验证环境SCADE,目前多用于开发嵌入式安全关键系统的软件。经过30多年的发展,逐渐在航空航天、国防军工、汽车电子等行业具有了广泛应用[17-19]。SCADE能够覆盖软件开发的全部流程[20]。SCADE建模分为安全状态机模型和数据流图模型,都属于图形建模方法。两种方式不是独立存在的,可以结合使用。二者相比较,状态机更适用于控制流方面的建模,在同样精准地描述控制算法的前提下,更加易于扩展维护[21]。

2 场景安全验证方法流程

2.1 场景安全验证方法流程

基于STAMP理论与模型检验的复杂运营场景安全验证框架主要包括三部分:基于STAMP理论和STPA方法的运营场景安全分析、运营场景安全状态机形式化模型的构建、运营场景的形式化安全验证。总体验证框架如图2所示。

图2 总体验证框架

本文的验证过程主要分为以下5个步骤。

步骤1:运营场景分层控制结构模型的构建。针对具体运营场景,首先确定可能发生的系统级事故及危险,提取运营场景中涉及到的控制器、执行器、传感器、被控过程以及交互信息等建模要素,遵循分层控制结构模型自上而下的建模顺序,确定顶层控制器,并根据各个组件的信息交互行为,逐级构建运营场景的分层控制结构模型。以便后续分析导致系统层面危险发生的致因因素。

步骤2:辨识导致危险发生的不安全控制行为。分层控制结构模型表现了系统或场景中控制器和执行器的控制行为,结合分层控制结构模型以及相关场景规范,通过上述4种不恰当控制行为的分类,辨识场景中的不安全控制行为。

步骤3:危险致因分析及安全约束提取。针对潜在的危险,结合分层控制结构模型,构建过程模型细化分析,确定导致不安全控制行为发生的致因因素,并提取相应的安全约束。

步骤4:运营场景安全状态机建模。通过提取运营场景分层控制结构模型中的模型要素,基于分层控制结构模型与安全状态机模型之间的转换规则,充分考虑运营场景安全约束,利用安全状态机建模方法,在SCADE环境中,构建可形式化验证的安全状态机模型。

步骤5:运营场景安全验证。利用数据流图建模方法,针对提取的运营场景安全约束,构建相应的安全属性模型,通过SCADE形式化工具,结合模型检验技术,对运营场景下的安全状态机模型进行形式化安全验证。

2.2 分层控制结构模型与安全状态机模型间转换规则

根据分层控制结构模型与安全状态机模型的定义和特点,给出了两种模型之间的基本转换规则定义。在构建的过程中,变量的名称可以根据实际所需要的内容自行定义,结合实际设计方式进行扩展。

当安全状态机的一个状态创建完成后,需要对其属性进行设置,通常包括状态机名称、起始状态以及终止状态等。转换过程的第一步需要根据状态机的状态内行为设计方式的不同,将状态机划分为4种类型[22],分别如下。

(1)无行为逻辑的状态机,也就是没有添加行为逻辑的状态机。

(2)嵌套基于模型设计的状态机,用于行为元素能够被状态布局完全容纳的情况下,常见于将数据流图嵌套于状态机内。

(3)嵌套SCADE文本设计的状态机,用于控制行为便于用SCADE文本表达的情况。

(4)隐藏文本内容的状态机,用于行为元素无法被状态布局容纳的情况下。

分层控制结构模型能够表现待分析系统或场景中交互主体的通信关系、信息交互内容等。其核心结构有控制器、执行器、传感器、被控过程等。基于此,定义以下规则,模型转换基本原则如图3所示。

图3 模型转换规则示意

规则1:控制器需要接收高层次部件发出的命令,并向低层次部件发出命令,针对控制器的行为逻辑,将其构建为嵌套SCADE文本的SSM。

规则2:系统中执行器需要发送信息至下一级控制器或自身状态需要根据接收到的命令改变,针对执行器的行为逻辑结合实际场景,将其构建为嵌套SCADE文本的SSM或嵌套基于模型设计的SSM。

规则3:传感器作为两层控制器之间的信息反馈装置,根据需要反馈的信息类型,结合实际场景构建为无行为逻辑的SSM或嵌套基于模型设计的SSM。

规则4:被控过程构建为无行为逻辑的SSM。

规则5:控制器发出或接收的命令、执行器需要执行的命令以及自身状态变化、组件间的交互信息、传感器反馈的信息等内容被提取为迁移条件或迁移行为,当信息内容为时序相关或只需要在迁移触发时执行的,将其构建为BOOL表达式,位于迁移线上;当信息内容需要在状态激活时的每一个周期执行时,例如一个控制器处于激活态时,它就需要发送相应的命令至下一级控制器或执行器,诸如此类的命令信息可以将其设置为枚举或其他类型,构建为SCADE赋值语句嵌套于对应的SSM中。

3 列车自动进站停车场景安全分析

进站停车场景是全自动无人驾驶场景中正线运营时的场景之一。当列车确认收到满足进站条件的移动授权,站台门关闭,紧急停车按钮未按下,人员防护开关SPKS置于非防护位,这4个条件满足时,列车可以进站。在该场景中列车需要完成自动驾驶进站精准停车;欠标或过标时根据距离的不同,设置不同的运行模式最终对标停车;安全打开站台门及车门,确保车门与站台门对位隔离,对应打开或关闭。

3.1 列车自动进站停车场景描述

根据相关技术规范,对列车进站停车场景进行描述[23-24]。该流程包括参加系统活动的对象,主要是各个子系统及设备。主要的交互信息如图4所示。

图4 进站停车场景活动图

场景主要流程说明如下。

(1)控制中心将线路相关信息发送至车载控制器VOBC,并提供临时限速。

(2)车载控制器VOBC确认线路信息并发送列车相关信息至区域控制器ZC,ZC需确认收到并根据信息计算移动授权MA。

(3)当确认收到移动授权,站台门关闭,紧急停车按钮未按下,人员防护开关SPKS置于非防护位,这4个条件满足后,列车可以进站停车。

(4)输出制动,判断车辆停车位置是否位于允许范围内,若未超过允许范围,停车成功;若车辆超过允许范围,先输出紧急制动,判断车辆过标/欠标是否超过5 m,若未超过5 m,则缓解紧急制动,并自动调整对标停车;若超过5 m,则不能缓解紧急制动,并通知人工上车救援,以人工模式停车。

(5)判断车辆速度为0后,判断站台门是否发生故障,若发现故障,则及时屏蔽相应的车门。车载控制器VOBC向车门控制器发送开门信息,向计算机联锁系统CI发送站台门打开信息。

(6)车门控制器收到信息并打开车门,确认状态,向车载控制器VOBC反馈信息;同时计算机联锁系统发送开门信息至站台门控制器,站台门控制器收到信息打开站台门并确认状态,反馈至计算机联锁系统。

(7)控制中心向站台广播系统发送信息,站台广播进行播报。

3.2 列车进站停车危险分析

根据进站停车场景分析,可能发生的系统级事故如下。

A1:乘客受伤(开关门过程中夹伤等)。

A2:列车追尾。

A3:列车与障碍物相撞。

事故A1的相关危险主要是在列车车门开关过程中出现的,可能由于列车车门动作的异常,例如,车门的开启时间异常或没有及时屏蔽出现故障的车门。针对事故A2和A3,列车运行时,通过接收区域控制器发送的移动授权,确定列车停车的目标点。当列车运行速度超过了能够防护本列车在前方列车车尾或障碍物前停车的速度最大值时,将会导致危险。

针对上述三类事故,给出在进站停车场景中的系统级危险如下。

H1:车门动作异常(可能导致A1)。

H2:列车进站时超速(可能导致A2、A3)。

3.3 系统分层控制结构模型

根据对列车自动进站停车场景流程的定义和分解,提取场景中担任控制器、执行器、被控过程的部分,在进站停车场景中,主要的上层控制器为车载控制器、控制中心、区域控制器、计算机联锁。各控制器需要发送相关指令或场景所需要的信息至下一层结构。车门控制器及站台门控制器担任执行器的作用,处理上层控制器发送的命令并对下一层的控制器或执行器发出指令。车门、站台门及列车根据实际场景需求,提取为被控过程进行建模。构建完成的分层控制结构模型如图5所示。

图5 进站停车分层控制结构模型

3.4 不安全控制行为

根据分层控制结构模型中各控制器的控制行为,并结合以下4种通用分类,辨识不安全控制行为UCA(Unsafe Control Action),由于本文篇幅限制,表1给出了部分辨识结果。

表1 部分不安全控制行为辨识结果

3.5 致因分析

以H1为例,给出部分致因分析结果及安全约束如表2所示。首先构建针对车门控制的过程模型,如图6所示。

表2 部分致因分析结果及安全约束

图6 车门控制过程模型

4 列车自动进站停车场景的安全状态机建模与安全属性验证

4.1 进站停车场景的安全状态机模型

根据进站停车场景流程以及提炼的主要建模步骤,首先确定安全状态机模型的基本框架,同时充分考虑安全分析中提取的安全约束内容,通过对进站停车场景的分层控制结构模型的定义和分解,分别提取在进站停车场景的分层控制结构模型中担任控制器、执行器、传感器以及被控过程的部分,利用上述定义的两种模型之间的转换规则,设置安全状态机的形态;提取的通信信息的部分,根据时序类、命令类或被控部分自身状态变化等实际情况的需要,构建为迁移条件或位于状态内的赋值语句。安全状态机模型部分变量类型及含义如表3所示,构建完成的安全状态机模型如图7所示。

表3 部分变量类型及含义

图7 进站停车场景的安全状态机模型

4.2 安全属性模型构建

以系统级危险H1为例,给出安全验证的过程。由上述安全分析可知,STPA识别的针对H1的不安全控制行为如下。

UCA1:紧急制动未缓解时车门开启。

UCA2:站台门发生故障时未隔离相应车门。

由于紧急制动未缓解,在该场景中是因为列车欠/过标5 m以上导致的,此时并未申请人工救援,列车不处于安全停车范围内,如果此时打开车门将会导致危险。

针对UCA1,提取安全约束:“列车紧急制动未缓解时,VOBC不能发送开门信息至车门和CI”,进行形式化验证分析。针对UCA2,提取安全约束:“检测到站台门故障未隔离相应车门时,VOBC不能发送开门信息至车门和CI”,进行形式化验证分析。

以UCA1的安全约束为例,涉及到模型中的变量有:车载控制器发送开门信息(VOBC_Door_Message)和列车紧急制动(Em_Breaking)。当模型输出为true,也就是1时,表示情况安全,输出为false,也就是0时,表示不安全情况发生。表4为这一安全约束下相关变量取值时,输出res的真假情况。

表4 安全约束的相关变量真值

根据表4,对于提取的安全约束将通过数据流图建模方式,构建为安全属性模型,如图8所示,按照同样的流程,构建针对UCA2的安全属性模型,如图9所示。

图8 针对UCA1的安全属性模型

图9 针对UCA2的安全属性模型

4.3 安全属性验证

当安全属性模型构建完成后,通过顶层操作符串联场景模型和安全属性模型,最后分析串联之后的模型输出。这种形式化的验证方法可以证明在待测模型中,安全属性在所有周期和场景下的正确性。如果模型有效,在检测结果一栏会显示为Valid;为Falsifiale时,则证明模型无效,SCADE将给出反例,可以通过单步测试或导入反例,以修改模型。

进站停车场景的形式化验证模型如图10所示,其中Package1::Operator1是初始状态机模型的集合形式,Operator3是安全属性观察模型的集合形式,将相应的变量连接起来,观测res输出。

图10 形式化验证模型

通过SCADE内置的验证器验证,模型分析用时1 s,检验结果为Valid。表示进站停车场景模型满足安全属性的观察模型,即该模型满足“在进站停车场景中,列车紧急制动未缓解时,车载控制器不能发送开门信息”这一安全约束。验证结果如图11所示。针对UCA2的安全约束,也进行上述验证。经过验证,检验结果为Valid,证明模型符合上述安全约束需求。根据STAMP系统安全理论及STPA安全分析方法可知,当场景满足安全约束时,证明对应的不安全控制行为没有发生,也就不会引发对应的系统级危险。

图11 模型验证结果

5 结论

本文在STAMP理论和STPA方法的基础上,结合安全状态机形式化建模方法与模型检验技术,提出了一种全自动无人驾驶复杂运营场景安全验证的方法,并以列车自动进站停车场景为例,对本文方法的可行性和有效性进行了验证分析,对于提高全自动无人驾驶系统的安全性具有重要的研究意义和应用价值,得出如下研究结论。

(1)将STAMP系统安全理论与安全状态机形式化建模方法结合,充分发挥两者的优势,在充分辨识复杂运营场景潜在危险的同时,还可以对场景进行形式化安全验证。

(2)通过定义分层控制结构模型与安全状态机模型间的基本转换规则,能够降低复杂运营场景安全状态机模型建模的难度、保证系统安全分析模型与形式化模型间的一致性。

(3)在运营场景安全分析的基础上构建的安全状态机形式化模型满足系统安全约束,在全自动无人驾驶系统安全设计和安全改进的过程中具有重要应用价值。