一種準(zhǔn)確識別損失場景的STPA

鐘德明，宮浩原，孫睿

(北京航空航天大學(xué)可靠性與系統(tǒng)工程學(xué)院，北京 100191)

軟件的使用使得系統(tǒng)事故機(jī)理逐漸發(fā)生改變，傳統(tǒng)基于物理失效的安全理論漸露弊端。美國工程院院士，麻省理工學(xué)院航空航天系教授Leveson[1]提出“系統(tǒng)理論事故模型與過程”（system-theoretic accident mode l and processes，STAMP），該理論認(rèn)為系統(tǒng)安全性是系統(tǒng)涌現(xiàn)屬性（emergentproperty）（涌現(xiàn)屬性的概念來源于系統(tǒng)理論中“整體大于部分之和”的思想，是在系統(tǒng)部件交互過程中表現(xiàn)出來的屬性）。在STAMP 的基礎(chǔ)上Leveson 和Thomas[2]提出了“系統(tǒng)理論過程分析”（system-theoretic process analysis，STPA）。STPA 認(rèn)為：即使沒有物理失效，部件之間不安全的交互也可能導(dǎo)致事故。許多對比工作說明：STPA 不僅能識別傳統(tǒng)方法能夠識別的致因場景，而且還能識別傳統(tǒng)方法所不能識別的致因場景，這些新的致因場景往往與軟件相關(guān)，不存在物理失效[2]。

2018 年3 月，Leveson 和Thomas[2]發(fā)布了STPA Handbook，這是當(dāng)前STPA 標(biāo)準(zhǔn)制定、工業(yè)應(yīng)用、工具開發(fā)、方法改進(jìn)等工作所參照的主要文獻(xiàn)（為了與其他文獻(xiàn)提出的STPA 做出區(qū)別，STPA Handbook中描述的STPA 簡記為HSTPA）。

目前，STPA 已被多份標(biāo)準(zhǔn)采納，例如RTCA DO 356A：Airworthiness security methods and considerations[3]和ISO/PAS21448:Roadvehicles-safetyof the intended functionality(SOTIF)[4]。

1 STPA 方法改進(jìn)動態(tài)

HSTPA 主要包括4 個(gè)步驟:

步驟 1確定分析目標(biāo)。包括識別損失、識別系統(tǒng)級危險(xiǎn)、識別系統(tǒng)級安全約束及細(xì)化危險(xiǎn)。

步驟 2構(gòu)建層級化控制結(jié)構(gòu)模型。有效的控制結(jié)構(gòu)將對整個(gè)系統(tǒng)的行為施加約束。層級化控制結(jié)構(gòu)模型包括至少五類元素：控制器、被控過程、控制動作、反饋及其他部件之間的輸入輸出。其中控制器包括控制算法和過程模型。

步驟 3識別不安全控制動作。不安全控制動作（unsafe control action，UCA）是在特定上下文和最壞環(huán)境下導(dǎo)致危險(xiǎn)的控制動作。UCA 包括五部分：控制動作的發(fā)出者（Source）、控制動作本身（control action，CA）、不安全的類型（Type）、所屬的上下文（Context）及所關(guān)聯(lián)的危險(xiǎn)（link t o hazards）。不安全的類型（Type）包括“提供CA”、“未提供CA”、“過早提供CA”、“過晚提供CA”、“過早停止CA”、“過晚停止CA”等。

步驟 4識別損失場景。損失場景描述了導(dǎo)致不安全控制動作和危險(xiǎn)的致因因素（causal factor，CF）。對HSTPA 改進(jìn)方面的動態(tài)主要體現(xiàn)為STPA的形式化工作。

文獻(xiàn)[5-7]是較早研究STPA 形式化的文獻(xiàn)。其中，文獻(xiàn)[5]對不安全控制動作進(jìn)行了形式化定義，并被HSTPA 所采納。文獻(xiàn)[5]利用真值計(jì)算方法自動識別UCA，被后續(xù)多份文獻(xiàn)所采納，如文獻(xiàn)[8]。但由于不涉及致因因素的自動化識別，因此文獻(xiàn)[5]對STPA 自動化的提升作用有限。文獻(xiàn)[6]將“不安全類型”（Type）提煉為缺失（om ission）、誤犯（commission）兩類,并基于該分類給出了時(shí)間相關(guān)“不安全類型”的描述，這有助于形式化描述UCA，特別是時(shí)間相關(guān)UCA。文獻(xiàn)[7]使用有限狀態(tài)機(jī)描述系統(tǒng)信息，但只使用了有限狀態(tài)機(jī)的靜態(tài)信息，并且以人工方式使用，不能支撐復(fù)雜系統(tǒng)危險(xiǎn)致因因素的識別。文獻(xiàn)[9]將“四變量模型”用于STPA 的模型構(gòu)建，具有較好的系統(tǒng)抽象特征，有助于構(gòu)建簡潔通用的系統(tǒng)模型。在文獻(xiàn)[5-7]工作之后，逐步出現(xiàn)整合STPA 和形式化證明技術(shù)的工作。文獻(xiàn)[10-12]使用模型檢測[13]或定理證明技術(shù)對STPA 分析結(jié)果進(jìn)行分析，有助于驗(yàn)證系統(tǒng)性質(zhì)，但這類工作沒有涉及STPA本身的改進(jìn)。文獻(xiàn)[14-15]將模型檢測技術(shù)用于STPA。文獻(xiàn)[14]利用NuSMV確定控制缺陷，文獻(xiàn)[15]利用UPPAAL 驗(yàn)證系統(tǒng)是否存在某個(gè)UCA。

當(dāng)系統(tǒng)較復(fù)雜，如規(guī)模較大、交互關(guān)系較多、致因因素較多時(shí)，系統(tǒng)危險(xiǎn)的涌現(xiàn)特性更加突出，以HSTPA 為核心的現(xiàn)有技術(shù)缺乏準(zhǔn)確識別涌現(xiàn)損失場景的能力，主要原因是：

1）未在系統(tǒng)全部的行為中識別損失場景。具體表現(xiàn)有：①僅在傳感器和控制器中識別損失場景，如HSTPA 的第1 類損失場景[2]；②僅在作動器和被控過程中識別損失場景，如HSTPA 的第2 類損失場景[2]；③僅在系統(tǒng)的局部功能中識別損失場景；④未使用過程模型的行為。涌現(xiàn)特性是系統(tǒng)全部部件行為作為整體呈現(xiàn)的特性，在系統(tǒng)部分行為中識別損失場景可能“誤報(bào)”或“漏報(bào)”損失場景。

2）人工分析難以處理大規(guī)模狀態(tài)及遷移。因此，自動分析是識別較復(fù)雜系統(tǒng)損失場景的自然選擇。

3）術(shù)語定義和方法過程存在重要缺陷，給STPA的理解和實(shí)施帶來很多混亂。這些缺陷包括：①用于定義UCA 的控制動作是控制器發(fā)出的控制動作，而不是被控過程接收到的控制動作；②損失場景的定義只強(qiáng)調(diào)了致因因素而未強(qiáng)調(diào)形成過程；③將損失場景分為兩類，并且認(rèn)為第2 類損失場景不存在UCA。

這些缺陷導(dǎo)致的問題有：①所識別的損失場景并沒有體現(xiàn)UCA 和危險(xiǎn)的涌現(xiàn)過程；②由于UCA的定義缺陷導(dǎo)致所識別的損失場景可能是錯(cuò)誤的；③對HSTPA 描述的第2 類損失場景，HSTPA 認(rèn)為不存在UCA，這是一個(gè)錯(cuò)誤判斷。UCA 所使用的控制動作應(yīng)該是被控過程接收到的控制動作，此時(shí)第2 類損失場景也存在UCA。

由于HSTPA 是各種改進(jìn)工作的基準(zhǔn)，因此上述問題主要源于HSTPA。本文針對上述問題，圍繞術(shù)語定義、過程設(shè)計(jì)、自動執(zhí)行三方面給出了一種結(jié)合工業(yè)建模語言和模型檢測技術(shù)的STPA，期望實(shí)現(xiàn)的目標(biāo)是：①用戶易于建模和使用；②可以自動給出損失場景；③損失場景具有更高的準(zhǔn)確性。

2 一種改進(jìn)的STPA

為了便于描述，本文改進(jìn)的STPA 方法簡記為ISTPA（improved STPA）。ISTPA 與HSTPA 的主要不同在于：①利用有限狀態(tài)機(jī)描述系統(tǒng)模型行為；②利用模型檢測技術(shù)識別損失場景。主要的差異及改進(jìn)原因如表1 所示，另外本節(jié)后續(xù)正文亦闡述了一些相對細(xì)節(jié)的差異。

表1 ISTPA 和HSTPA 的主要差異Table 1 M ain differences between ISTPA and HSTPA

ISTPA 也包括4 步，具體如下。各步的關(guān)系如圖1所示，其中步驟4 包括若干小步。

圖1 ISTPA的步驟Fig.1 Steps of ISTPA

步驟 1確定分析目標(biāo)。ISTPA 在本步驟中的內(nèi)容與HSTPA 中步驟1 的內(nèi)容基本相同。但優(yōu)化了“系統(tǒng)級危險(xiǎn)”的定義。HSTPA 對系統(tǒng)級危險(xiǎn)的定義：“危險(xiǎn)是在最壞環(huán)境條件下可能導(dǎo)致?lián)p失的系統(tǒng)狀態(tài)或條件集合”。由于危險(xiǎn)未必是在“最壞環(huán)境條件”下才發(fā)生，且“最壞環(huán)境條件”難以進(jìn)行形式化描述，因此，ISTPA 將定義改為：“系統(tǒng)級危險(xiǎn)是在特定條件下能夠?qū)е聯(lián)p失的系統(tǒng)狀態(tài)”。

步驟 2構(gòu)建系統(tǒng)狀態(tài)機(jī)。HSTPA 通過框、線元素描述層級化控制結(jié)構(gòu)，對系統(tǒng)的動態(tài)行為缺乏描述，為了彌補(bǔ)這項(xiàng)不足，ISTPA 采用有限狀態(tài)機(jī)描述層級化控制結(jié)構(gòu)中的行為。描述行為的方式有很多，比如順序圖、活動圖、PetriNet 等，但鑒于以下原因，采用有限狀態(tài)機(jī)描述系統(tǒng)行為。

1）有限狀態(tài)機(jī)具備足夠的行為描述能力。有限狀態(tài)機(jī)不僅可以描述系統(tǒng)的高層行為，也可以描述部件內(nèi)的細(xì)節(jié)行為。在ISTPA 中，識別UCA 和識別損失場景所需要的系統(tǒng)行為全部可以使用狀態(tài)機(jī)描述，包括控制器行為、被控過程行為、傳感器行為、作動器行為及他們之間的交互關(guān)系，其中控制器行為又包括過程模型行為和控制算法。將過程模型的行為納入有限狀態(tài)機(jī)是ISTPA 對HSTPA的一項(xiàng)重要改進(jìn)，這樣可以構(gòu)建完整的系統(tǒng)行為模型，方便識別具有涌現(xiàn)特征的損失場景。

用于識別不安全控制動作的系統(tǒng)狀態(tài)機(jī)可以只包括控制器狀態(tài)機(jī)、被控過程狀態(tài)機(jī)及他們之間的交互關(guān)系，用于識別損失場景的系統(tǒng)狀態(tài)機(jī)包括控制器狀態(tài)機(jī)、被控過程狀態(tài)機(jī)、傳感器狀態(tài)機(jī)、作動器狀態(tài)機(jī)及他們之間的交互關(guān)系。

2）有限狀態(tài)機(jī)是工業(yè)界常用的建模技術(shù)。Sys-ML、AADL、AltaRica 都支持有限狀態(tài)機(jī)建模，這有助于ISTPA 與已有系統(tǒng)工程工作融合，復(fù)用已有成果，降低建模工作量，減少重構(gòu)模型帶來的語義變化，提高分析的準(zhǔn)確性。

步驟 3識別UCA。首先，ISTPA 對HSTPA 中的UCA 概念進(jìn)行了澄清。HSTPA 沒有明確規(guī)定UCA中控制動作所處的位置，但似乎默認(rèn)控制動作處于控制器的輸出位置，這給后續(xù)損失場景分析帶來了混亂。在ISTPA 中，UCA 是控制動作（controlactionprocess received，CA-PR）、不安全的類型（Type）、上下文（Context）之間的組合{CA-PR、Type、Context}，并且這個(gè)組合在特定條件下能夠?qū)е孪到y(tǒng)級危險(xiǎn)。ISTPA 規(guī)定UCA 的CA-PR 處于被控過程的輸入位置。這樣處理的原因是，控制器發(fā)出的控制動作可能因作動器、輸出線路等原因?qū)е屡c被控過程實(shí)際收到的控制動作不同，比如時(shí)間延遲、信息改變，而在判斷被控過程的狀態(tài)時(shí)應(yīng)當(dāng)以實(shí)際收到的控制動作為準(zhǔn)。

每個(gè)CA-PR 的屬性包括該CA-PR 的發(fā)出者、接收者及其他數(shù)據(jù)定義。當(dāng)系統(tǒng)狀態(tài)機(jī)中不包括作動器時(shí)，CA-PR 既處于被控過程的輸入位置，也處于控制器的輸出位置。當(dāng)系統(tǒng)狀態(tài)機(jī)中包括作動器時(shí)，CA-PR 則處于作動器的輸出位置和被控過程的輸入位置。在識別UCA 時(shí)，首先，給出{CA-PR、Type、Context}的所有實(shí)例，每個(gè){CA-PR、Type、Context}的實(shí)例都被認(rèn)為是一個(gè)潛在不安全控制動作（potential UCA，PUCA）。然后，逐一分析每一個(gè)PUCA，確定其是否為UCA。當(dāng)1 個(gè)PUCA 確定為UCA 時(shí)，該UCA 將是以下2 種情況中的1 種：①UCA 可以追蹤到一個(gè)已被識別的系統(tǒng)級危險(xiǎn)，不需要更新已識別的系統(tǒng)級危險(xiǎn)；②UCA 不能追蹤到一個(gè)已識別的系統(tǒng)級危險(xiǎn)，需要依據(jù)該UCA 補(bǔ)充系統(tǒng)級危險(xiǎn)。

步驟 4識別損失場景。在HSTPA 中，損失場景的定義：“損失場景描述了導(dǎo)致UCA 和危險(xiǎn)的致因因素”。ISTPA 將損失場景的定義改為：“損失場景是系統(tǒng)在致因因素參與下產(chǎn)生系統(tǒng)級危險(xiǎn)的過程”。損失場景描述了系統(tǒng)通過涌現(xiàn)行為形成系統(tǒng)級危險(xiǎn)的過程。致因因素是與危險(xiǎn)發(fā)生相關(guān)的因素，致因因素很多，例如：硬件失效、軟件缺陷、數(shù)據(jù)偏差、數(shù)據(jù)錯(cuò)誤、過程模型錯(cuò)誤、部件交互、模式變化、環(huán)境變化、環(huán)境干擾、被控過程變化、反饋缺失或錯(cuò)誤、反饋延遲、作動器失效或延遲等。

對于較復(fù)雜的系統(tǒng)，損失場景實(shí)際是危險(xiǎn)的涌現(xiàn)過程，因此很難通過人工方式識別。幸運(yùn)地是，形式化分析技術(shù)的“反例”（counterexample）功能可以用于求解危險(xiǎn)涌現(xiàn)過程。在現(xiàn)有形式化分析技術(shù)中，由于模型檢測技術(shù)相對定理證明技術(shù)較易使用，并且有較多成熟工具可供開源或免費(fèi)使用，因此，ISTPA 選擇模型檢測技術(shù)作為危險(xiǎn)涌現(xiàn)求解技術(shù)。

模型檢測是一種自動驗(yàn)證技術(shù)，構(gòu)成要素包括待檢測模型、待檢驗(yàn)性質(zhì)和模型檢測算法。模型檢測技術(shù)能在數(shù)學(xué)上證明待檢測模型是否滿足待檢測性質(zhì)，如果不能滿足則通過“反例”展示待檢測模型如何運(yùn)行以致違反待檢測性質(zhì)?！胺蠢笔谴龣z測模型的一條運(yùn)行狀態(tài)軌跡，表明待檢測模型如何從初始狀態(tài)演變成違反待檢測性質(zhì)時(shí)的狀態(tài)[11]。

將系統(tǒng)安全性約束轉(zhuǎn)變成待檢測性質(zhì)，將系統(tǒng)狀態(tài)機(jī)轉(zhuǎn)換成待檢測模型，則利用模型檢測技術(shù)獲得的“反例”就是損失場景。

用于識別損失場景的系統(tǒng)狀態(tài)機(jī)相對于識別UCA 的系統(tǒng)狀態(tài)機(jī)主要有以下不同：①前者包括了傳感器和作動器，后者一般不包括傳感器和作動器；②前者相對后者可以添加致因因素。

3 ISTPA 應(yīng)用示例

第2 節(jié)對ISTPA 的描述較抽象，本節(jié)結(jié)合示例具體演示ISTPA 的應(yīng)用過程。由于在現(xiàn)有STPA 形式化技術(shù)研究中常以列車門控制為例，如文獻(xiàn)[6-7]，為便于理解，本文也以列車門控制為例。

步驟 1確定分析目標(biāo)。為了說明原理，本文做了簡化，只考慮列車靜止并且車門對準(zhǔn)站臺時(shí)的相關(guān)損失和危險(xiǎn)。這些信息是后續(xù)分析的輸入，主要依據(jù)經(jīng)驗(yàn)確定，結(jié)果如下：①損失L：門擠壓門道上的人或物，導(dǎo)致人、物、門損傷。②系統(tǒng)級危險(xiǎn)H1：當(dāng)門處于完全打開狀態(tài)，并且門道存在障礙物時(shí)，門收到關(guān)門命令。③系統(tǒng)級安全性約束SCH1：當(dāng)門處于完全打開狀態(tài)，并且門道存在障礙物時(shí)，門不能收到關(guān)門命令。

步驟 2構(gòu)建系統(tǒng)狀態(tài)機(jī)。為系統(tǒng)建立“系統(tǒng)建模語言”（systems model ing language，SysML）的系統(tǒng)狀態(tài)機(jī)圖。在SysML 系統(tǒng)狀態(tài)機(jī)圖的“General”屬性中定義全局變量及其初始值。在SysML 系統(tǒng)狀態(tài)機(jī)圖中添加State Machine 元素，為控制器、被控過程、傳感器、作動器構(gòu)建狀態(tài)機(jī)。用于識別不安全控制動作的系統(tǒng)狀態(tài)機(jī)可以只包括控制器狀態(tài)機(jī)、被控過程狀態(tài)機(jī)及他們之間的交互關(guān)系。

General 屬性中定義的全局變量如表2 所示。

表2 SysM L 系統(tǒng)狀態(tài)機(jī)圖中的全局變量Table 2 G lobal variables in SysM L state m achine diagram

系統(tǒng)狀態(tài)機(jī)圖包含司機(jī)、列車門控制器、列車門、障礙物4 個(gè)子狀態(tài)機(jī)。

①司機(jī)狀態(tài)機(jī)如圖2(a)所示。有1 個(gè)idle 狀態(tài)和2 條Transition，Initial 元 素 指 向idle 狀 態(tài)，2 條Transition 由于均為同步遷移，分別用Synch 元素指向，其中synDriverClose 表示司機(jī)向列車門控制器發(fā)出關(guān)門指令，synDriverOpen 表示司機(jī)向列車門控制器發(fā)送開門指令。②列車門控制器狀態(tài)機(jī)如圖2(b)所示。列車門控制器接收司機(jī)的開門指令和關(guān)門指令并對列車門發(fā)出開門命令和關(guān)門命令，并且在障礙物出現(xiàn)在門道時(shí)，會發(fā)出開門命令。具體的元素類型與司機(jī)狀態(tài)機(jī)圖類似。③列車門狀態(tài)機(jī)如圖2(c)所示。列車門包含完全關(guān)閉、開門過程、完全打開和關(guān)門過程4 個(gè)狀態(tài)，由于列車門開門過程和關(guān)門過程需要時(shí)間，因此，需要描述相關(guān)的時(shí)間信息。本文采用“實(shí)時(shí)嵌入式系統(tǒng)建模和分析 剖 面” (modeling and analysis of real time and embedded systems，MARTE)元素來進(jìn)行描述。以physicalOpening 狀態(tài)為例，指向遷入轉(zhuǎn)移的Clock-Constraint 元素表示對tDoorOpening 時(shí)鐘變量進(jìn)行更新，開始計(jì)時(shí)；指向狀態(tài)的TimedConstraint 元素表示在physicalOpening 狀態(tài)需要滿足的時(shí)間約束，即tDoorOpening≤10；指向遷出轉(zhuǎn)移的TimedConstraint 元素表示遷移發(fā)生需要滿足的時(shí)間約束，即tDoorOpening≥10；上述3 個(gè)MARTE 元素的組合表示開門時(shí)間為10 個(gè)時(shí)間單位。關(guān)門過程同樣需要10 個(gè)時(shí)間單位。④障礙物狀態(tài)機(jī)如圖2(d)所示。門道中存在或不存在障礙物。

圖2 列車門控制系統(tǒng)SysML狀態(tài)機(jī)(用于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}，并且這個(gè)組合能夠?qū)е履硞€(gè)系統(tǒng)級危險(xiǎn)。該危險(xiǎn)可能是本節(jié)步驟1 中已識別的危險(xiǎn)或其子危險(xiǎn)，也可能是一項(xiàng)尚未被識別的新危險(xiǎn)。

列車門控制器提供的控制動作CA 包括：開門命令（Open Command），關(guān)門命令（Cl ose Command）。由于此時(shí)系統(tǒng)狀態(tài)機(jī)不包括作動器，因此CA 與CA-PR 相 同。CA-PR 可 取 值 有Open Command 或Close Command。

UCA 的類型包括，Type1：不提供控制動作導(dǎo)致危險(xiǎn)；Type2：提供控制動作導(dǎo)致危險(xiǎn)；Type3：提供一個(gè)控制動作，但是提供得過早、過晚或錯(cuò)誤順序；Type4：控制動作持續(xù)太長或結(jié)束太快，適用于連續(xù)控制動作，而不是離散控制動作)。因此類型的可取值有Type1、Type2、Type3、Type4。

2）根據(jù)SysML 系統(tǒng)狀態(tài)機(jī)確定Context 的上下文變量及其可能的取值，列出Context 全部實(shí)例。

上下文變量分別是列車門狀態(tài)PhysicalDoor 和障礙物狀態(tài)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}的所有實(shí)例。每個(gè){CA-PR，Type，Context}的實(shí)例都被認(rèn)為是一個(gè)PUCA。包含時(shí)間無關(guān)“類型”的PUCA被稱為時(shí)間無關(guān)PUCA，包含時(shí)間相關(guān)“類型”的PUCA 被稱為時(shí)間相關(guān)PUCA。

PUCA={CA-PR,Context,Type}，共有64 種情況。作為示例，僅列舉了少數(shù)幾種情況，如圖3 所示。

4）根據(jù)本節(jié)步驟1 確定的損失，逐一分析每一個(gè)PUCA，確定其是否為UCA。

圖3 的64 種情況逐一分析，分析結(jié)果見表3。

圖3 列車門控制系統(tǒng)潛在不安全控制動作Fig.3 Potential UCAs of train door control system

以表3 中ID 為1 和55 的PUCA 為例，說明分析過程。ID 為1 的PUCA，即列車門控制器在列車門處于完全打開狀態(tài)（PhysicalDoor=Opened）且障礙物位于門道（PhysicalBlock=Blocked）時(shí)，列車門收到了（Type=Providing）關(guān)門命令（CA-PR=CloseCommand），是本節(jié)步驟1 已經(jīng)標(biāo)識的危險(xiǎn)H1，因此在表3 的Hazard 列填寫H1。

表3 潛在不安全控制動作分析結(jié)果Tab le 3 Analysis results of potential UCAs

ID 為55 的PUCA，即列車門控制器在列車門處于關(guān)閉過程狀態(tài)（PhysicalDoor=Closing）且障礙物位于門道（PhysicalBlock=Blocked）時(shí)，列車門太晚（Type=Too early,toolate,outof order）收到開門命令（CA-PR=Open Command），系統(tǒng)將出現(xiàn)危險(xiǎn)。該危險(xiǎn)未出現(xiàn)在已標(biāo)識危險(xiǎn)中，是一處新增危險(xiǎn)。本文將其標(biāo)記為H2。根據(jù)系統(tǒng)的設(shè)計(jì)要求，將“太晚”的含義確定為晚于2 個(gè)時(shí)間單位。

至此，系統(tǒng)級危險(xiǎn)更新為2 個(gè)，分別是H1 和H2。H1：門處于完全打開狀態(tài)時(shí)，并且門道存在障礙物時(shí)，門收到關(guān)門命令。H2:門處于關(guān)閉過程時(shí)，并且門道存在障礙物時(shí)，門晚于2 個(gè)時(shí)間單位收到開門命令。由于是示例，本文后續(xù)僅保留H2，認(rèn)為只要系統(tǒng)能夠避免H2 發(fā)生，即使發(fā)生H1 也無關(guān)緊要。

步驟 4識別損失場景。

1）更新步驟2 所形成的系統(tǒng)狀態(tài)機(jī)。更新后的系統(tǒng)狀態(tài)機(jī)包括控制器狀態(tài)機(jī)、被控過程狀態(tài)機(jī)、傳感器狀態(tài)機(jī)、作動器狀態(tài)機(jī)及他們之間的交互關(guān)系，也包括控制器、被控過程、傳感器、作動器內(nèi)部子部件的狀態(tài)機(jī)及子部件之間的交互關(guān)系。

更新后的系統(tǒng)狀態(tài)機(jī)全局變量如表4 所示。

表4 更新后全局變量Table 4 Updated global variables

更新后的列車門控制器狀態(tài)機(jī)發(fā)生了變化，由原來的直接向列車門發(fā)出控制命令轉(zhuǎn)為向列車門作動器發(fā)出開門命令和關(guān)門命令。變化后狀態(tài)機(jī)如圖4(a)所示。更新后的列車門狀態(tài)機(jī)同樣發(fā)生了變化，由原來的直接接收列車門控制器的命令改為接收列車門作動器的信號輸出，同時(shí)反饋信號改為經(jīng)由列車門傳感器傳遞。變化后的列車門狀態(tài)機(jī)如圖4(b)所示。列車門作動器狀態(tài)機(jī)如圖4(c)所示，用于接收列車門控制器發(fā)出的關(guān)門命令和開門命令，向列車門輸出關(guān)門信號和開門信號。障礙物傳感器狀態(tài)機(jī)如圖4(d)所示，用于感知障礙物是否處于門道，并向列車門控制器發(fā)送相應(yīng)的信息。列車門傳感器狀態(tài)機(jī)如圖4(e)所示，用于感知列車門的狀態(tài)，向列車門控制器發(fā)送相應(yīng)的列車門狀態(tài)信息。司機(jī)和障礙物狀態(tài)機(jī)相對本節(jié)步驟2 未發(fā)生變化，因此不再展示。

圖4 增加作動器和傳感器后發(fā)生變化的狀態(tài)機(jī)(用于損失場景識別)Fig.4 State machine after addition of actuators and sensors (For identifying loss scenarios)

2）根據(jù)步驟4 第1 步中更新后的系統(tǒng)狀態(tài)機(jī)形成模型檢測模型。列車門控制器UPPAALTemplate如圖5(a)所示。列車門作動器UPPAAL Template 如圖5(b)所示。列車門UPPAAL Template 如圖5(c)所示，其中clear()和start()函數(shù)分別對時(shí)鐘變量counter進(jìn)行清零和開始計(jì)時(shí)；block 變量為布爾值，true 表示障礙物位于門道，false 表示障礙物不位于門道；counter 是為了記錄障礙物出現(xiàn)至列車門轉(zhuǎn)為打開狀態(tài)這一過程的時(shí)間而定義的時(shí)鐘變量；SysML 系統(tǒng)狀態(tài)機(jī)中沒有直接表達(dá)counter、clear()、start()等詳細(xì)信息內(nèi)容的變量和函數(shù)，為了驗(yàn)證安全性約束，因此在UPPAAL Template 中添加了上述變量和函數(shù)。列車門傳感器UPPAAL Template 如圖5(d)所示。司機(jī)UPPAAL Template 如圖5(e)所示。障礙物UPPAAL Template 如圖5(f)所示，其中start()函數(shù)的引入是為了驗(yàn)證安全性約束，start()函數(shù)用于對時(shí)鐘變量counter 開始計(jì)時(shí)。障礙物傳感器UPPAAL Template 如圖5(g)所示。

圖5 增加作動器和傳感器后的UPPAAL模型(用于損失場景識別)Fig.5 The UPPAAL model after addition of actuators and sensors (For identifying loss scenarios)

3）根據(jù)系統(tǒng)級危險(xiǎn)確定系統(tǒng)的安全性約束，并使用模型檢測技術(shù)支持的邏輯語言描述安全性約束，形成待檢測性質(zhì)；本步結(jié)束之后，每條系統(tǒng)級危險(xiǎn)對應(yīng)一條系統(tǒng)的安全性約束，而每條系統(tǒng)的安全性約束又對應(yīng)一條待檢測性質(zhì)。根據(jù)步驟3 確認(rèn)的系統(tǒng)級危險(xiǎn)H2，確定相應(yīng)的系統(tǒng)安全性約束：

SCH2：門處于關(guān)閉過程時(shí)，并且門道存在障礙物時(shí)，門必須在2 個(gè)時(shí)間單位內(nèi)收到開門指令。

再將安全性約束轉(zhuǎn)換為TCTL 約束，即待檢測性質(zhì)。SpecH2表示安全性約束SCH2的TCTL 表達(dá)規(guī)范（Specification）。

SpecH2:A[]not(PhysicalDoor.physicalClosing and PhysicalBlock.physicalBlock andcounter＆gt;2)

4）利用模型檢測技術(shù)分析步驟2 所形成的模型檢測模型是否滿足步驟3 所形成的待檢測性質(zhì)，如果違反，模型檢測技術(shù)自動給出反例，該反例即為導(dǎo)致系統(tǒng)級危險(xiǎn)的損失場景。

實(shí)際驗(yàn)證結(jié)果表明UPPAAL 模型滿足SpecH2這條性質(zhì)，進(jìn)而表明步驟4 第1 步建立的更新后的系統(tǒng)狀態(tài)機(jī)模型滿足安全性約束SCH2。

5）生成“增加CF 的經(jīng)更新的系統(tǒng)狀態(tài)機(jī)”，將其轉(zhuǎn)換成模型檢測模型，并對待檢測性質(zhì)進(jìn)行檢測。

增加CF 的方案有很多，不能窮舉，因此，可能要依據(jù)經(jīng)驗(yàn)限制方案的數(shù)量，例如，可以依據(jù)CF 的發(fā)生概率確定增加CF 的方案。

在步驟4 第1 步所建立的經(jīng)更新的系統(tǒng)狀態(tài)機(jī)中，障礙物傳感器和列車門作動器的信號轉(zhuǎn)換和傳輸不存在延遲。作為示例，在這里通過改變狀態(tài)機(jī)狀態(tài)和遷移，分別向障礙物傳感器和列車門作動器注入1～2 個(gè)時(shí)間單位的信號傳輸延遲，共計(jì)2 個(gè)CF，形成增加CF 的SysML 系統(tǒng)狀態(tài)機(jī)。

向障礙物傳感器狀態(tài)機(jī)注入信號延遲方法：

新定義局部時(shí)鐘變量tBlockSensorDelay，用來表達(dá)障礙物傳感器延遲時(shí)間，增加了一個(gè)中間狀態(tài)（見圖6(a)左上狀態(tài)），在遷入該狀態(tài)的Transition元素的“Effect”屬性中添加“ClockConstraint”元素，并將tBlockSensorDelay 置0，在中間狀態(tài)的“Invariant”約束屬性中添加“TimedConstraint”元素（tBlockSensorDelay≤2），在遷出該狀態(tài)的Transition 元素“Guard”屬性中添加“TimedConstraint”元素（tBlockSensor-Delay≥1），通過上述元素共同表達(dá)障礙物傳感器從接收到synBlock 信號到發(fā)出synBlockSensorOutput-Block 信號的延遲為1～2 個(gè)時(shí)間單位。注入延遲后的障礙物傳感器狀態(tài)機(jī)如圖6(a)所示。

向列車門作動器狀態(tài)機(jī)注入開門信號延遲方法：

新定義局部時(shí)鐘變量tActuatorDelay，用來表達(dá)列車門作動器延遲時(shí)間，增加一個(gè)中間狀態(tài)（見圖6(b)上部狀態(tài)），在遷入該狀態(tài)的Transition 元素“Effect”屬性中添加“ClockConstraint”元素，并將tActuatorDelay置0，在中間狀態(tài)的“Invariant”約束屬性中添加“TimedConstraint”元素（tActuatorDelay≤2），在遷出該狀態(tài)的Transition 元素“Guard”屬性中添加“Timed-Constraint”元素（tActuatorDelay≥1），通過上述元素共同表達(dá)列車門控制器從接收到synControllerOutput-Command 信號到輸出開門信號（actuatorOutput=1）的延遲為1～2 個(gè)時(shí)間單位。注入延遲后列車門作動器狀態(tài)機(jī)如圖6(b)所示。利用“增加CF 的經(jīng)更新的系統(tǒng)狀態(tài)機(jī)”生成模型檢測模型。由于其他狀態(tài)機(jī)保持不變，此處僅展示注入CF 的障礙物傳感器和列車門作動器所對應(yīng)的UPPAAL 模型。注入延遲后列車門作動器UPPAAL Template 如圖7(a)所示。注入延遲后障礙物傳感器UPPAAL Template如圖7(b)所示。對注入CF 的UPPAAL 模型進(jìn)行驗(yàn)證。實(shí)際驗(yàn)證結(jié)果表明UPPAAL 模型不滿足性質(zhì)SpecH2，進(jìn)而表明“增加CF 的SysML 系統(tǒng)狀態(tài)機(jī)”不滿足安全性約束SCH2。

圖6 增加CF的SysML系統(tǒng)狀態(tài)機(jī)（用于損失場景識別）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 系統(tǒng)出現(xiàn)H2的一條損失場景Fig.8 A loss scenario leading to H2

（1）司機(jī)發(fā)出開門指令（synDriverOpen）；

（2）列車門控制器接收到指令后，向列車門作動器發(fā)出開門命令（synControllerOutputOpenCommand）；

（3）列車門作動器作動器收到開門命令后，延遲1～2 個(gè)時(shí)間單位，向列車門輸出開門信號（synActuatorOutputOpenAction）；

（4）隨后列車門由關(guān)閉狀態(tài)（physicalClosed）轉(zhuǎn)為開門過程狀態(tài)（physicalOpening），同時(shí)列車門傳感器也轉(zhuǎn)為感知開門過程狀態(tài)（sensedOpening）；

（5）經(jīng)過10 個(gè)時(shí)間單位后，在作動器控制信號未變的情況下（actuatorOutput=1），列車門轉(zhuǎn)為完全打開狀態(tài)（physicalOpened），同時(shí)列車門傳感器也轉(zhuǎn)為感知完全打開狀態(tài)（sensedOpened）；

（6）接著司機(jī)發(fā)出關(guān)門指令（synDriverClose）；

（7）列車門控制器向列車門作動器發(fā)出關(guān)門命令（synControllerOutputCloseCommand）；

（8）列車門作動器輸出關(guān)門信號（synActuator-OutputCloseAction）；

（9）隨后列車門由完全打開狀態(tài)（physicalOpened）轉(zhuǎn)為關(guān)門過程狀態(tài)（physicalClosing），同時(shí)列車門傳感器也轉(zhuǎn)為感知關(guān)門過程狀態(tài)（sensedClosing）；

（10）障礙物出現(xiàn)在門道，門道處于存在障礙物的狀態(tài)（PhysicalBlock），障礙物傳感器接收到syn-Block 信號，此時(shí)counter 由start()函數(shù)置0，開始計(jì)時(shí)；

（11）障礙物傳感器向列車門控制器發(fā)送syn-BlockSensorOutputBlock 信號過程存在1～2 個(gè)時(shí)間單位延遲，因此counter 此刻記錄了1～2 個(gè)時(shí)間單位；

（12）列車門控制器發(fā)出開門命令（synControllerOutputOpenCommand）；

（13）由于列車門作動器輸出開門信號過程存在1～2 個(gè)時(shí)間單位延遲，因此counter 此刻記錄了2～4 個(gè)時(shí)間單位，表示從門道內(nèi)存在障礙物到列車門接收到開門命令經(jīng)過了2～4 個(gè)時(shí)間單位。

此時(shí)，列車門處于關(guān)門過程狀態(tài)（physicalClosing），門道處于存在障礙物的狀態(tài)（physicalBlock），從門道內(nèi)存在障礙物到列車門接收到開門命令經(jīng)過的時(shí)間（counter）大于2 個(gè)時(shí)間單位，SpecH2被違反，系統(tǒng)處于危險(xiǎn)狀態(tài)。

這個(gè)損失場景包含了向障礙物傳感器和列車門作動器注入的2 個(gè)與信號傳輸延遲有關(guān)的CF，他們共同作用，在系統(tǒng)的交互運(yùn)行中導(dǎo)致危險(xiǎn)。

4 對比分析

圖9 展示了使用HSTPA 和ISTPA 分別對4 種方案的分析結(jié)果。

圖9 應(yīng)用示例分析結(jié)果比較Fig.9 Comparison of the analysis results of the example

對于方案1，由于不存在CF，因此HSTPA 認(rèn)為無需分析損失場景。但實(shí)際上，沒有CF 注入的情況，系統(tǒng)仍然可能有損失場景，這就是所謂的“即使全部部件正常，其交互也可能導(dǎo)致危險(xiǎn)”。ISTPA可以對無CF 注入的系統(tǒng)進(jìn)行分析，針對方案1 所得出的結(jié)果是“不存在損失場景”。

HSTPA 將損失場景分為成兩類：第1 類損失場景在傳感器和控制器中進(jìn)行分析，第2 類損失場景在作動器和被控過程中進(jìn)行分析。方案2 所注入的CF 存在于傳感器，屬于HSTPA 第1 類損失場景的范疇。方案3 所注入的CF 存在于作動器，因此屬于第2 類損失場景的范疇。HSTPA 可以針對方案2 和3 給出人工定性分析結(jié)果，即“可能存在損失場景”，但不能給出確定答案，分析結(jié)果難以驗(yàn)證。與此不同，ISTPA 確定地認(rèn)為系統(tǒng)不存在損失場景。

方案4 同時(shí)注入傳感器致因因素和作動器致因因素，ISTPA 通過對傳感器、控制器、作動器、被控過程等全部部件所構(gòu)成的整體行為進(jìn)行分析，發(fā)現(xiàn)所注入的2 個(gè)致因因素恰恰參與了1 條損失場景的形成，更好地體現(xiàn)了涌現(xiàn)特性的分析能力。而HSTPA 對兩類損失場景的劃分導(dǎo)致其只能在局部部件中識別損失場景，因此無法識別系統(tǒng)全部部件交互可能形成的損失場景。

5 結(jié) 論

1）HSTPA 在損失場景準(zhǔn)確性方面存在以下問題：存在“漏報(bào)”和“誤報(bào)”問題；不能明確判斷損失場景是否發(fā)生，不能準(zhǔn)確描述損失場景的形成過程。

2）ISTPA 可以具體、完整地描述損失場景的形成過程，可以分析沒有增加CF 的系統(tǒng)損失場景，也可以分析包括全部部件的系統(tǒng)損失場景，減少了“漏報(bào)”和“誤報(bào)”問題，體現(xiàn)了更準(zhǔn)確的損失場景識別能力。