钟德明,宫浩原,孙睿
(北京航空航天大学可靠性与系统工程学院,北京 100191)
软件的使用使得系统事故机理逐渐发生改变,传统基于物理失效的安全理论渐露弊端。美国工程院院士,麻省理工学院航空航天系教授Leveson[1]提出“系统理论事故模型与过程”(system-theoretic accident mode l and processes,STAMP),该理论认为系统安全性是系统涌现属性(emergentproperty)(涌现属性的概念来源于系统理论中“整体大于部分之和”的思想,是在系统部件交互过程中表现出来的属性)。在STAMP 的基础上Leveson 和Thomas[2]提出了“系统理论过程分析”(system-theoretic process analysis,STPA)。STPA 认为:即使没有物理失效,部件之间不安全的交互也可能导致事故。许多对比工作说明:STPA 不仅能识别传统方法能够识别的致因场景,而且还能识别传统方法所不能识别的致因场景,这些新的致因场景往往与软件相关,不存在物理失效[2]。
2018 年3 月,Leveson 和Thomas[2]发布了STPA Handbook,这是当前STPA 标准制定、工业应用、工具开发、方法改进等工作所参照的主要文献(为了与其他文献提出的STPA 做出区别,STPA Handbook中描述的STPA 简记为HSTPA)。
目前,STPA 已被多份标准采纳,例如RTCA DO 356A:Airworthiness security methods and considerations[3]和ISO/PAS21448:Roadvehicles-safetyof the intended functionality(SOTIF)[4]。
HSTPA 主要包括4 个步骤:
步骤 1确定分析目标。包括识别损失、识别系统级危险、识别系统级安全约束及细化危险。
步骤 2构建层级化控制结构模型。有效的控制结构将对整个系统的行为施加约束。层级化控制结构模型包括至少五类元素:控制器、被控过程、控制动作、反馈及其他部件之间的输入输出。其中控制器包括控制算法和过程模型。
步骤 3识别不安全控制动作。不安全控制动作(unsafe control action,UCA)是在特定上下文和最坏环境下导致危险的控制动作。UCA 包括五部分:控制动作的发出者(Source)、控制动作本身(control action,CA)、不安全的类型(Type)、所属的上下文(Context)及所关联的危险(link t o hazards)。不安全的类型(Type)包括“提供CA”、“未提供CA”、“过早提供CA”、“过晚提供CA”、“过早停止CA”、“过晚停止CA”等。
步骤 4识别损失场景。损失场景描述了导致不安全控制动作和危险的致因因素(causal factor,CF)。对HSTPA 改进方面的动态主要体现为STPA的形式化工作。
文献[5-7]是较早研究STPA 形式化的文献。其中,文献[5]对不安全控制动作进行了形式化定义,并被HSTPA 所采纳。文献[5]利用真值计算方法自动识别UCA,被后续多份文献所采纳,如文献[8]。但由于不涉及致因因素的自动化识别,因此文献[5]对STPA 自动化的提升作用有限。文献[6]将“不安全类型”(Type)提炼为缺失(om ission)、误犯(commission)两类,并基于该分类给出了时间相关“不安全类型”的描述,这有助于形式化描述UCA,特别是时间相关UCA。文献[7]使用有限状态机描述系统信息,但只使用了有限状态机的静态信息,并且以人工方式使用,不能支撑复杂系统危险致因因素的识别。文献[9]将“四变量模型”用于STPA 的模型构建,具有较好的系统抽象特征,有助于构建简洁通用的系统模型。在文献[5-7]工作之后,逐步出现整合STPA 和形式化证明技术的工作。文献[10-12]使用模型检测[13]或定理证明技术对STPA 分析结果进行分析,有助于验证系统性质,但这类工作没有涉及STPA本身的改进。文献[14-15]将模型检测技术用于STPA。文献[14]利用NuSMV确定控制缺陷,文献[15]利用UPPAAL 验证系统是否存在某个UCA。
当系统较复杂,如规模较大、交互关系较多、致因因素较多时,系统危险的涌现特性更加突出,以HSTPA 为核心的现有技术缺乏准确识别涌现损失场景的能力,主要原因是:
1)未在系统全部的行为中识别损失场景。具体表现有:①仅在传感器和控制器中识别损失场景,如HSTPA 的第1 类损失场景[2];
②仅在作动器和被控过程中识别损失场景,如HSTPA 的第2 类损失场景[2];
③仅在系统的局部功能中识别损失场景;
④未使用过程模型的行为。涌现特性是系统全部部件行为作为整体呈现的特性,在系统部分行为中识别损失场景可能“误报”或“漏报”损失场景。
2)人工分析难以处理大规模状态及迁移。因此,自动分析是识别较复杂系统损失场景的自然选择。
3)术语定义和方法过程存在重要缺陷,给STPA的理解和实施带来很多混乱。这些缺陷包括:①用于定义UCA 的控制动作是控制器发出的控制动作,而不是被控过程接收到的控制动作;
②损失场景的定义只强调了致因因素而未强调形成过程;
③将损失场景分为两类,并且认为第2 类损失场景不存在UCA。
这些缺陷导致的问题有:①所识别的损失场景并没有体现UCA 和危险的涌现过程;
②由于UCA的定义缺陷导致所识别的损失场景可能是错误的;
③对HSTPA 描述的第2 类损失场景,HSTPA 认为不存在UCA,这是一个错误判断。UCA 所使用的控制动作应该是被控过程接收到的控制动作,此时第2 类损失场景也存在UCA。
由于HSTPA 是各种改进工作的基准,因此上述问题主要源于HSTPA。本文针对上述问题,围绕术语定义、过程设计、自动执行三方面给出了一种结合工业建模语言和模型检测技术的STPA,期望实现的目标是:①用户易于建模和使用;
②可以自动给出损失场景;
③损失场景具有更高的准确性。
为了便于描述,本文改进的STPA 方法简记为ISTPA(improved STPA)。ISTPA 与HSTPA 的主要不同在于:①利用有限状态机描述系统模型行为;
②利用模型检测技术识别损失场景。主要的差异及改进原因如表1 所示,另外本节后续正文亦阐述了一些相对细节的差异。
表1 ISTPA 和HSTPA 的主要差异Table 1 M ain differences between ISTPA and HSTPA
ISTPA 也包括4 步,具体如下。各步的关系如图1所示,其中步骤4 包括若干小步。
图1 ISTPA的步骤Fig.1 Steps of ISTPA
步骤 1确定分析目标。ISTPA 在本步骤中的内容与HSTPA 中步骤1 的内容基本相同。但优化了“系统级危险”的定义。HSTPA 对系统级危险的定义:“危险是在最坏环境条件下可能导致损失的系统状态或条件集合”。由于危险未必是在“最坏环境条件”下才发生,且“最坏环境条件”难以进行形式化描述,因此,ISTPA 将定义改为:“系统级危险是在特定条件下能够导致损失的系统状态”。
步骤 2构建系统状态机。HSTPA 通过框、线元素描述层级化控制结构,对系统的动态行为缺乏描述,为了弥补这项不足,ISTPA 采用有限状态机描述层级化控制结构中的行为。描述行为的方式有很多,比如顺序图、活动图、PetriNet 等,但鉴于以下原因,采用有限状态机描述系统行为。
1)有限状态机具备足够的行为描述能力。有限状态机不仅可以描述系统的高层行为,也可以描述部件内的细节行为。在ISTPA 中,识别UCA 和识别损失场景所需要的系统行为全部可以使用状态机描述,包括控制器行为、被控过程行为、传感器行为、作动器行为及他们之间的交互关系,其中控制器行为又包括过程模型行为和控制算法。将过程模型的行为纳入有限状态机是ISTPA 对HSTPA的一项重要改进,这样可以构建完整的系统行为模型,方便识别具有涌现特征的损失场景。
用于识别不安全控制动作的系统状态机可以只包括控制器状态机、被控过程状态机及他们之间的交互关系,用于识别损失场景的系统状态机包括控制器状态机、被控过程状态机、传感器状态机、作动器状态机及他们之间的交互关系。
2)有限状态机是工业界常用的建模技术。Sys-ML、AADL、AltaRica 都支持有限状态机建模,这有助于ISTPA 与已有系统工程工作融合,复用已有成果,降低建模工作量,减少重构模型带来的语义变化,提高分析的准确性。
步骤 3识别UCA。首先,ISTPA 对HSTPA 中的UCA 概念进行了澄清。HSTPA 没有明确规定UCA中控制动作所处的位置,但似乎默认控制动作处于控制器的输出位置,这给后续损失场景分析带来了混乱。在ISTPA 中,UCA 是控制动作(controlactionprocess received,CA-PR)、不安全的类型(Type)、上下文(Context)之间的组合{CA-PR、Type、Context},并且这个组合在特定条件下能够导致系统级危险。ISTPA 规定UCA 的CA-PR 处于被控过程的输入位置。这样处理的原因是,控制器发出的控制动作可能因作动器、输出线路等原因导致与被控过程实际收到的控制动作不同,比如时间延迟、信息改变,而在判断被控过程的状态时应当以实际收到的控制动作为准。
每个CA-PR 的属性包括该CA-PR 的发出者、接收者及其他数据定义。当系统状态机中不包括作动器时,CA-PR 既处于被控过程的输入位置,也处于控制器的输出位置。当系统状态机中包括作动器时,CA-PR 则处于作动器的输出位置和被控过程的输入位置。在识别UCA 时,首先,给出{CA-PR、Type、Context}的所有实例,每个{CA-PR、Type、Context}的实例都被认为是一个潜在不安全控制动作(potential UCA,PUCA)。然后,逐一分析每一个PUCA,确定其是否为UCA。当1 个PUCA 确定为UCA 时,该UCA 将是以下2 种情况中的1 种:①UCA 可以追踪到一个已被识别的系统级危险,不需要更新已识别的系统级危险;
②UCA 不能追踪到一个已识别的系统级危险,需要依据该UCA 补充系统级危险。
步骤 4识别损失场景。在HSTPA 中,损失场景的定义:“损失场景描述了导致UCA 和危险的致因因素”。ISTPA 将损失场景的定义改为:“损失场景是系统在致因因素参与下产生系统级危险的过程”。损失场景描述了系统通过涌现行为形成系统级危险的过程。致因因素是与危险发生相关的因素,致因因素很多,例如:硬件失效、软件缺陷、数据偏差、数据错误、过程模型错误、部件交互、模式变化、环境变化、环境干扰、被控过程变化、反馈缺失或错误、反馈延迟、作动器失效或延迟等。
对于较复杂的系统,损失场景实际是危险的涌现过程,因此很难通过人工方式识别。幸运地是,形式化分析技术的“反例”(counterexample)功能可以用于求解危险涌现过程。在现有形式化分析技术中,由于模型检测技术相对定理证明技术较易使用,并且有较多成熟工具可供开源或免费使用,因此,ISTPA 选择模型检测技术作为危险涌现求解技术。
模型检测是一种自动验证技术,构成要素包括待检测模型、待检验性质和模型检测算法。模型检测技术能在数学上证明待检测模型是否满足待检测性质,如果不能满足则通过“反例”展示待检测模型如何运行以致违反待检测性质。“反例”是待检测模型的一条运行状态轨迹,表明待检测模型如何从初始状态演变成违反待检测性质时的状态[11]。
将系统安全性约束转变成待检测性质,将系统状态机转换成待检测模型,则利用模型检测技术获得的“反例”就是损失场景。
用于识别损失场景的系统状态机相对于识别UCA 的系统状态机主要有以下不同:①前者包括了传感器和作动器,后者一般不包括传感器和作动器;
②前者相对后者可以添加致因因素。
第2 节对ISTPA 的描述较抽象,本节结合示例具体演示ISTPA 的应用过程。由于在现有STPA 形式化技术研究中常以列车门控制为例,如文献[6-7],为便于理解,本文也以列车门控制为例。
步骤 1确定分析目标。为了说明原理,本文做了简化,只考虑列车静止并且车门对准站台时的相关损失和危险。这些信息是后续分析的输入,主要依据经验确定,结果如下:①损失L:门挤压门道上的人或物,导致人、物、门损伤。②系统级危险H1:当门处于完全打开状态,并且门道存在障碍物时,门收到关门命令。③系统级安全性约束SCH1:当门处于完全打开状态,并且门道存在障碍物时,门不能收到关门命令。
步骤 2构建系统状态机。为系统建立“系统建模语言”(systems model ing language,SysML)的系统状态机图。在SysML 系统状态机图的“General”属性中定义全局变量及其初始值。在SysML 系统状态机图中添加State Machine 元素,为控制器、被控过程、传感器、作动器构建状态机。用于识别不安全控制动作的系统状态机可以只包括控制器状态机、被控过程状态机及他们之间的交互关系。
General 属性中定义的全局变量如表2 所示。
表2 SysM L 系统状态机图中的全局变量Table 2 G lobal variables in SysM L state m achine diagram
系统状态机图包含司机、列车门控制器、列车门、障碍物4 个子状态机。
①司机状态机如图2(a)所示。有1 个idle 状态和2 条Transition,Initial 元 素 指 向idle 状 态,2 条Transition 由于均为同步迁移,分别用Synch 元素指向,其中synDriverClose 表示司机向列车门控制器发出关门指令,synDriverOpen 表示司机向列车门控制器发送开门指令。②列车门控制器状态机如图2(b)所示。列车门控制器接收司机的开门指令和关门指令并对列车门发出开门命令和关门命令,并且在障碍物出现在门道时,会发出开门命令。具体的元素类型与司机状态机图类似。③列车门状态机如图2(c)所示。列车门包含完全关闭、开门过程、完全打开和关门过程4 个状态,由于列车门开门过程和关门过程需要时间,因此,需要描述相关的时间信息。本文采用“实时嵌入式系统建模和分析 剖 面” (modeling and analysis of real time and embedded systems,MARTE)元素来进行描述。以physicalOpening 状态为例,指向迁入转移的Clock-Constraint 元素表示对tDoorOpening 时钟变量进行更新,开始计时;
指向状态的TimedConstraint 元素表示在physicalOpening 状态需要满足的时间约束,即tDoorOpening≤10;
指向迁出转移的TimedConstraint 元素表示迁移发生需要满足的时间约束,即tDoorOpening≥10;
上述3 个MARTE 元素的组合表示开门时间为10 个时间单位。关门过程同样需要10 个时间单位。④障碍物状态机如图2(d)所示。门道中存在或不存在障碍物。
图2 列车门控制系统SysML状态机(用于UCA识别)Fig.2 SysML state machine of train door control system (For identifying UCAs)
步骤 3识别不安全控制动作。
1)将UCA 定义为被控过程接收到的控制动作(control action,CA-PR)、UCA 的类型(Type)、上下文(Context)之间的组合{CA-PR、Type、Context},并且这个组合能够导致某个系统级危险。该危险可能是本节步骤1 中已识别的危险或其子危险,也可能是一项尚未被识别的新危险。
列车门控制器提供的控制动作CA 包括:开门命令(Open Command),关门命令(Cl ose Command)。由于此时系统状态机不包括作动器,因此CA 与CA-PR 相 同。CA-PR 可 取 值 有Open Command 或Close Command。
UCA 的类型包括,Type1:不提供控制动作导致危险;
Type2:提供控制动作导致危险;
Type3:提供一个控制动作,但是提供得过早、过晚或错误顺序;
Type4:控制动作持续太长或结束太快,适用于连续控制动作,而不是离散控制动作)。因此类型的可取值有Type1、Type2、Type3、Type4。
2)根据SysML 系统状态机确定Context 的上下文变量及其可能的取值,列出Context 全部实例。
上下文变量分别是列车门状态PhysicalDoor 和障碍物状态PhysicalBlock,Context={PhysicalDoor,PhysicalBlock}。PhysicalDoor 可 取 值 有1:Closing;
2:Opening;
3:Closed;
4:Opened。PhysicalBlock 可 取值有1:NotBlocked;
2:Blocked。因此,Context可取元素有(1,1)、(1,2)、(2,1)、(2,2)、(3,1)、(3,2)、(4,1)、(4,2)。
3)通过遍历,给出{CA-PR,Type,Context}的所有实例。每个{CA-PR,Type,Context}的实例都被认为是一个PUCA。包含时间无关“类型”的PUCA被称为时间无关PUCA,包含时间相关“类型”的PUCA 被称为时间相关PUCA。
PUCA={CA-PR,Context,Type},共有64 种情况。作为示例,仅列举了少数几种情况,如图3 所示。
4)根据本节步骤1 确定的损失,逐一分析每一个PUCA,确定其是否为UCA。
图3 的64 种情况逐一分析,分析结果见表3。
图3 列车门控制系统潜在不安全控制动作Fig.3 Potential UCAs of train door control system
以表3 中ID 为1 和55 的PUCA 为例,说明分析过程。ID 为1 的PUCA,即列车门控制器在列车门处于完全打开状态(PhysicalDoor=Opened)且障碍物位于门道(PhysicalBlock=Blocked)时,列车门收到了(Type=Providing)关门命令(CA-PR=CloseCommand),是本节步骤1 已经标识的危险H1,因此在表3 的Hazard 列填写H1。
表3 潜在不安全控制动作分析结果Tab le 3 Analysis results of potential UCAs
ID 为55 的PUCA,即列车门控制器在列车门处于关闭过程状态(PhysicalDoor=Closing)且障碍物位于门道(PhysicalBlock=Blocked)时,列车门太晚(Type=Too early,toolate,outof order)收到开门命令(CA-PR=Open Command),系统将出现危险。该危险未出现在已标识危险中,是一处新增危险。本文将其标记为H2。根据系统的设计要求,将“太晚”的含义确定为晚于2 个时间单位。
至此,系统级危险更新为2 个,分别是H1 和H2。H1:门处于完全打开状态时,并且门道存在障碍物时,门收到关门命令。H2:门处于关闭过程时,并且门道存在障碍物时,门晚于2 个时间单位收到开门命令。由于是示例,本文后续仅保留H2,认为只要系统能够避免H2 发生,即使发生H1 也无关紧要。
步骤 4识别损失场景。
1)更新步骤2 所形成的系统状态机。更新后的系统状态机包括控制器状态机、被控过程状态机、传感器状态机、作动器状态机及他们之间的交互关系,也包括控制器、被控过程、传感器、作动器内部子部件的状态机及子部件之间的交互关系。
更新后的系统状态机全局变量如表4 所示。
表4 更新后全局变量Table 4 Updated global variables
更新后的列车门控制器状态机发生了变化,由原来的直接向列车门发出控制命令转为向列车门作动器发出开门命令和关门命令。变化后状态机如图4(a)所示。更新后的列车门状态机同样发生了变化,由原来的直接接收列车门控制器的命令改为接收列车门作动器的信号输出,同时反馈信号改为经由列车门传感器传递。变化后的列车门状态机如图4(b)所示。列车门作动器状态机如图4(c)所示,用于接收列车门控制器发出的关门命令和开门命令,向列车门输出关门信号和开门信号。障碍物传感器状态机如图4(d)所示,用于感知障碍物是否处于门道,并向列车门控制器发送相应的信息。列车门传感器状态机如图4(e)所示,用于感知列车门的状态,向列车门控制器发送相应的列车门状态信息。司机和障碍物状态机相对本节步骤2 未发生变化,因此不再展示。
图4 增加作动器和传感器后发生变化的状态机(用于损失场景识别)Fig.4 State machine after addition of actuators and sensors (For identifying loss scenarios)
2)根据步骤4 第1 步中更新后的系统状态机形成模型检测模型。列车门控制器UPPAALTemplate如图5(a)所示。列车门作动器UPPAAL Template 如图5(b)所示。列车门UPPAAL Template 如图5(c)所示,其中clear()和start()函数分别对时钟变量counter进行清零和开始计时;
block 变量为布尔值,true 表示障碍物位于门道,false 表示障碍物不位于门道;
counter 是为了记录障碍物出现至列车门转为打开状态这一过程的时间而定义的时钟变量;
SysML 系统状态机中没有直接表达counter、clear()、start()等详细信息内容的变量和函数,为了验证安全性约束,因此在UPPAAL Template 中添加了上述变量和函数。列车门传感器UPPAAL Template 如图5(d)所示。司机UPPAAL Template 如图5(e)所示。障碍物UPPAAL Template 如图5(f)所示,其中start()函数的引入是为了验证安全性约束,start()函数用于对时钟变量counter 开始计时。障碍物传感器UPPAAL Template 如图5(g)所示。
图5 增加作动器和传感器后的UPPAAL模型(用于损失场景识别)Fig.5 The UPPAAL model after addition of actuators and sensors (For identifying loss scenarios)
3)根据系统级危险确定系统的安全性约束,并使用模型检测技术支持的逻辑语言描述安全性约束,形成待检测性质;
本步结束之后,每条系统级危险对应一条系统的安全性约束,而每条系统的安全性约束又对应一条待检测性质。根据步骤3 确认的系统级危险H2,确定相应的系统安全性约束:
SCH2:门处于关闭过程时,并且门道存在障碍物时,门必须在2 个时间单位内收到开门指令。
再将安全性约束转换为TCTL 约束,即待检测性质。SpecH2表示安全性约束SCH2的TCTL 表达规范(Specification)。
SpecH2:A[]not(PhysicalDoor.physicalClosing and PhysicalBlock.physicalBlock andcounter>2)
4)利用模型检测技术分析步骤2 所形成的模型检测模型是否满足步骤3 所形成的待检测性质,如果违反,模型检测技术自动给出反例,该反例即为导致系统级危险的损失场景。
实际验证结果表明UPPAAL 模型满足SpecH2这条性质,进而表明步骤4 第1 步建立的更新后的系统状态机模型满足安全性约束SCH2。
5)生成“增加CF 的经更新的系统状态机”,将其转换成模型检测模型,并对待检测性质进行检测。
增加CF 的方案有很多,不能穷举,因此,可能要依据经验限制方案的数量,例如,可以依据CF 的发生概率确定增加CF 的方案。
在步骤4 第1 步所建立的经更新的系统状态机中,障碍物传感器和列车门作动器的信号转换和传输不存在延迟。作为示例,在这里通过改变状态机状态和迁移,分别向障碍物传感器和列车门作动器注入1~2 个时间单位的信号传输延迟,共计2 个CF,形成增加CF 的SysML 系统状态机。
向障碍物传感器状态机注入信号延迟方法:
新定义局部时钟变量tBlockSensorDelay,用来表达障碍物传感器延迟时间,增加了一个中间状态(见图6(a)左上状态),在迁入该状态的Transition元素的“Effect”属性中添加“ClockConstraint”元素,并将tBlockSensorDelay 置0,在中间状态的“Invariant”约束属性中添加“TimedConstraint”元素(tBlockSensorDelay≤2),在迁出该状态的Transition 元素“Guard”属性中添加“TimedConstraint”元素(tBlockSensor-Delay≥1),通过上述元素共同表达障碍物传感器从接收到synBlock 信号到发出synBlockSensorOutput-Block 信号的延迟为1~2 个时间单位。注入延迟后的障碍物传感器状态机如图6(a)所示。
向列车门作动器状态机注入开门信号延迟方法:
新定义局部时钟变量tActuatorDelay,用来表达列车门作动器延迟时间,增加一个中间状态(见图6(b)上部状态),在迁入该状态的Transition 元素“Effect”属性中添加“ClockConstraint”元素,并将tActuatorDelay置0,在中间状态的“Invariant”约束属性中添加“TimedConstraint”元素(tActuatorDelay≤2),在迁出该状态的Transition 元素“Guard”属性中添加“Timed-Constraint”元素(tActuatorDelay≥1),通过上述元素共同表达列车门控制器从接收到synControllerOutput-Command 信号到输出开门信号(actuatorOutput=1)的延迟为1~2 个时间单位。注入延迟后列车门作动器状态机如图6(b)所示。利用“增加CF 的经更新的系统状态机”生成模型检测模型。由于其他状态机保持不变,此处仅展示注入CF 的障碍物传感器和列车门作动器所对应的UPPAAL 模型。注入延迟后列车门作动器UPPAAL Template 如图7(a)所示。注入延迟后障碍物传感器UPPAAL Template如图7(b)所示。对注入CF 的UPPAAL 模型进行验证。实际验证结果表明UPPAAL 模型不满足性质SpecH2,进而表明“增加CF 的SysML 系统状态机”不满足安全性约束SCH2。
图6 增加CF的SysML系统状态机(用于损失场景识别)Fig.6 SysML state machine after addition of CFs (For identifying loss scenarios)
图7 增加CF后更新的UPPAAL模型(用于损失场景识别)Fig.7 UPPAAL model after addition of CFs (For identifying loss scenarios)
违反SpecH2的一条反例(即损失场景)如图8 所示,其过程如下:
图8 系统出现H2的一条损失场景Fig.8 A loss scenario leading to H2
(1)司机发出开门指令(synDriverOpen);
(2)列车门控制器接收到指令后,向列车门作动器发出开门命令(synControllerOutputOpenCommand);
(3)列车门作动器作动器收到开门命令后,延迟1~2 个时间单位,向列车门输出开门信号(synActuatorOutputOpenAction);
(4)随后列车门由关闭状态(physicalClosed)转为开门过程状态(physicalOpening),同时列车门传感器也转为感知开门过程状态(sensedOpening);
(5)经过10 个时间单位后,在作动器控制信号未变的情况下(actuatorOutput=1),列车门转为完全打开状态(physicalOpened),同时列车门传感器也转为感知完全打开状态(sensedOpened);
(6)接着司机发出关门指令(synDriverClose);
(7)列车门控制器向列车门作动器发出关门命令(synControllerOutputCloseCommand);
(8)列车门作动器输出关门信号(synActuator-OutputCloseAction);
(9)随后列车门由完全打开状态(physicalOpened)转为关门过程状态(physicalClosing),同时列车门传感器也转为感知关门过程状态(sensedClosing);
(10)障碍物出现在门道,门道处于存在障碍物的状态(PhysicalBlock),障碍物传感器接收到syn-Block 信号,此时counter 由start()函数置0,开始计时;
(11)障碍物传感器向列车门控制器发送syn-BlockSensorOutputBlock 信号过程存在1~2 个时间单位延迟,因此counter 此刻记录了1~2 个时间单位;
(12)列车门控制器发出开门命令(synControllerOutputOpenCommand);
(13)由于列车门作动器输出开门信号过程存在1~2 个时间单位延迟,因此counter 此刻记录了2~4 个时间单位,表示从门道内存在障碍物到列车门接收到开门命令经过了2~4 个时间单位。
此时,列车门处于关门过程状态(physicalClosing),门道处于存在障碍物的状态(physicalBlock),从门道内存在障碍物到列车门接收到开门命令经过的时间(counter)大于2 个时间单位,SpecH2被违反,系统处于危险状态。
这个损失场景包含了向障碍物传感器和列车门作动器注入的2 个与信号传输延迟有关的CF,他们共同作用,在系统的交互运行中导致危险。
图9 展示了使用HSTPA 和ISTPA 分别对4 种方案的分析结果。
图9 应用示例分析结果比较Fig.9 Comparison of the analysis results of the example
对于方案1,由于不存在CF,因此HSTPA 认为无需分析损失场景。但实际上,没有CF 注入的情况,系统仍然可能有损失场景,这就是所谓的“即使全部部件正常,其交互也可能导致危险”。ISTPA可以对无CF 注入的系统进行分析,针对方案1 所得出的结果是“不存在损失场景”。
HSTPA 将损失场景分为成两类:第1 类损失场景在传感器和控制器中进行分析,第2 类损失场景在作动器和被控过程中进行分析。方案2 所注入的CF 存在于传感器,属于HSTPA 第1 类损失场景的范畴。方案3 所注入的CF 存在于作动器,因此属于第2 类损失场景的范畴。HSTPA 可以针对方案2 和3 给出人工定性分析结果,即“可能存在损失场景”,但不能给出确定答案,分析结果难以验证。与此不同,ISTPA 确定地认为系统不存在损失场景。
方案4 同时注入传感器致因因素和作动器致因因素,ISTPA 通过对传感器、控制器、作动器、被控过程等全部部件所构成的整体行为进行分析,发现所注入的2 个致因因素恰恰参与了1 条损失场景的形成,更好地体现了涌现特性的分析能力。而HSTPA 对两类损失场景的划分导致其只能在局部部件中识别损失场景,因此无法识别系统全部部件交互可能形成的损失场景。
1)HSTPA 在损失场景准确性方面存在以下问题:存在“漏报”和“误报”问题;
不能明确判断损失场景是否发生,不能准确描述损失场景的形成过程。
2)ISTPA 可以具体、完整地描述损失场景的形成过程,可以分析没有增加CF 的系统损失场景,也可以分析包括全部部件的系统损失场景,减少了“漏报”和“误报”问题,体现了更准确的损失场景识别能力。
猜你喜欢状态机障碍物损失胖胖损失了多少元数学小灵通·3-4年级(2021年5期)2021-07-16高低翻越动漫界·幼教365(中班)(2020年3期)2020-04-20SelTrac®CBTC系统中非通信障碍物的设计和处理铁道通信信号(2020年9期)2020-02-06基于有限状态机的交会对接飞行任务规划方法北京航空航天大学学报(2019年9期)2019-10-26玉米抽穗前倒伏怎么办?怎么减少损失?今日农业(2019年15期)2019-01-03一般自由碰撞的最大动能损失广西民族大学学报(自然科学版)(2015年3期)2015-12-07损失读者·校园版(2015年19期)2015-05-14双口RAM读写正确性自动测试的有限状态机控制器设计方法广西科技大学学报(2015年4期)2015-02-27土钉墙在近障碍物的地下车行通道工程中的应用城市道桥与防洪(2014年5期)2014-02-27基于反熔丝FPGA的有限状态机加固设计空间控制技术与应用(2010年5期)2010-12-23