一種準(zhǔn)確識(shí)別損失場(chǎng)景的STPA

鐘德明，宮浩原，孫睿

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

軟件的使用使得系統(tǒng)事故機(jī)理逐漸發(fā)生改變，傳統(tǒng)基于物理失效的安全理論漸露弊端。美國(guó)工程院院士，麻省理工學(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)致事故。許多對(duì)比工作說明：STPA 不僅能識(shí)別傳統(tǒng)方法能夠識(shí)別的致因場(chǎng)景，而且還能識(shí)別傳統(tǒng)方法所不能識(shí)別的致因場(chǎng)景，這些新的致因場(chǎ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 簡(jiǎn)記為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)動(dòng)態(tài)

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

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

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

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

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

文獻(xiàn)[5-7]是較早研究STPA 形式化的文獻(xiàn)。其中，文獻(xiàn)[5]對(duì)不安全控制動(dòng)作進(jìn)行了形式化定義，并被HSTPA 所采納。文獻(xiàn)[5]利用真值計(jì)算方法自動(dòng)識(shí)別UCA，被后續(xù)多份文獻(xiàn)所采納，如文獻(xiàn)[8]。但由于不涉及致因因素的自動(dòng)化識(shí)別，因此文獻(xiàn)[5]對(duì)STPA 自動(dòng)化的提升作用有限。文獻(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)致因因素的識(shí)別。文獻(xiàn)[9]將“四變量模型”用于STPA 的模型構(gòu)建，具有較好的系統(tǒng)抽象特征，有助于構(gòu)建簡(jiǎn)潔通用的系統(tǒng)模型。在文獻(xiàn)[5-7]工作之后，逐步出現(xiàn)整合STPA 和形式化證明技術(shù)的工作。文獻(xiàn)[10-12]使用模型檢測(cè)[13]或定理證明技術(shù)對(duì)STPA 分析結(jié)果進(jìn)行分析，有助于驗(yàn)證系統(tǒng)性質(zhì)，但這類工作沒有涉及STPA本身的改進(jìn)。文獻(xiàn)[14-15]將模型檢測(cè)技術(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)確識(shí)別涌現(xiàn)損失場(chǎng)景的能力，主要原因是：

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

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

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

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

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

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

為了便于描述，本文改進(jìn)的STPA 方法簡(jiǎn)記為ISTPA（improved STPA）。ISTPA 與HSTPA 的主要不同在于：①利用有限狀態(tài)機(jī)描述系統(tǒng)模型行為；②利用模型檢測(cè)技術(shù)識(shí)別損失場(chǎng)景。主要的差異及改進(jìn)原因如表1 所示，另外本節(jié)后續(xù)正文亦闡述了一些相對(duì)細(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)級(jí)危險(xiǎn)”的定義。HSTPA 對(duì)系統(tǒng)級(jí)危險(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)級(jí)危險(xiǎn)是在特定條件下能夠?qū)е聯(lián)p失的系統(tǒng)狀態(tài)”。

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

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

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

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

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

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

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

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

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

3 ISTPA 應(yīng)用示例

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

步驟 1確定分析目標(biāo)。為了說明原理，本文做了簡(jiǎn)化，只考慮列車靜止并且車門對(duì)準(zhǔn)站臺(tái)時(shí)的相關(guān)損失和危險(xiǎn)。這些信息是后續(xù)分析的輸入，主要依據(jù)經(jīng)驗(yàn)確定，結(jié)果如下：①損失L：門擠壓門道上的人或物，導(dǎo)致人、物、門損傷。②系統(tǒng)級(jí)危險(xiǎn)H1：當(dāng)門處于完全打開狀態(tài)，并且門道存在障礙物時(shí)，門收到關(guān)門命令。③系統(tǒng)級(jí)安全性約束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 元素，為控制器、被控過程、傳感器、作動(dòng)器構(gòu)建狀態(tài)機(jī)。用于識(shí)別不安全控制動(dòng)作的系統(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)門指令并對(duì)列車門發(fā)出開門命令和關(guān)門命令，并且在障礙物出現(xiàn)在門道時(shí)，會(huì)發(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 元素表示對(duì)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識(shí)別)Fig.2 SysML state machine of train door control system (For identifying UCAs)

步驟 3識(shí)別不安全控制動(dòng)作。

1）將UCA 定義為被控過程接收到的控制動(dòng)作（control action，CA-PR）、UCA 的類型（Type）、上下文（Context）之間的組合{CA-PR、Type、Context}，并且這個(gè)組合能夠?qū)е履硞€(gè)系統(tǒng)級(jí)危險(xiǎn)。該危險(xiǎn)可能是本節(jié)步驟1 中已識(shí)別的危險(xiǎn)或其子危險(xiǎn)，也可能是一項(xiàng)尚未被識(shí)別的新危險(xiǎn)。

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

UCA 的類型包括，Type1：不提供控制動(dòng)作導(dǎo)致危險(xiǎn)；Type2：提供控制動(dòng)作導(dǎo)致危險(xiǎn)；Type3：提供一個(gè)控制動(dòng)作，但是提供得過早、過晚或錯(cuò)誤順序；Type4：控制動(dòng)作持續(xù)太長(zhǎng)或結(jié)束太快，適用于連續(xù)控制動(dòng)作，而不是離散控制動(dòng)作)。因此類型的可取值有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)潛在不安全控制動(dò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)識(shí)的危險(xiǎn)H1，因此在表3 的Hazard 列填寫H1。

表3 潛在不安全控制動(dòng)作分析結(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)識(shí)危險(xiǎn)中，是一處新增危險(xiǎn)。本文將其標(biāo)記為H2。根據(jù)系統(tǒng)的設(shè)計(jì)要求，將“太晚”的含義確定為晚于2 個(gè)時(shí)間單位。

至此，系統(tǒng)級(jí)危險(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識(shí)別損失場(chǎng)景。

1）更新步驟2 所形成的系統(tǒng)狀態(tài)機(jī)。更新后的系統(tǒng)狀態(tài)機(jī)包括控制器狀態(tài)機(jī)、被控過程狀態(tài)機(jī)、傳感器狀態(tài)機(jī)、作動(dòng)器狀態(tài)機(jī)及他們之間的交互關(guān)系，也包括控制器、被控過程、傳感器、作動(dòng)器內(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)為向列車門作動(dòng)器發(fā)出開門命令和關(guān)門命令。變化后狀態(tài)機(jī)如圖4(a)所示。更新后的列車門狀態(tài)機(jī)同樣發(fā)生了變化，由原來的直接接收列車門控制器的命令改為接收列車門作動(dòng)器的信號(hào)輸出，同時(shí)反饋信號(hào)改為經(jīng)由列車門傳感器傳遞。變化后的列車門狀態(tài)機(jī)如圖4(b)所示。列車門作動(dòng)器狀態(tài)機(jī)如圖4(c)所示，用于接收列車門控制器發(fā)出的關(guān)門命令和開門命令，向列車門輸出關(guān)門信號(hào)和開門信號(hào)。障礙物傳感器狀態(tài)機(jī)如圖4(d)所示，用于感知障礙物是否處于門道，并向列車門控制器發(fā)送相應(yīng)的信息。列車門傳感器狀態(tài)機(jī)如圖4(e)所示，用于感知列車門的狀態(tài)，向列車門控制器發(fā)送相應(yīng)的列車門狀態(tài)信息。司機(jī)和障礙物狀態(tài)機(jī)相對(duì)本節(jié)步驟2 未發(fā)生變化，因此不再展示。

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

2）根據(jù)步驟4 第1 步中更新后的系統(tǒng)狀態(tài)機(jī)形成模型檢測(cè)模型。列車門控制器UPPAALTemplate如圖5(a)所示。列車門作動(dòng)器UPPAAL Template 如圖5(b)所示。列車門UPPAAL Template 如圖5(c)所示，其中clear()和start()函數(shù)分別對(duì)時(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ù)用于對(duì)時(shí)鐘變量counter 開始計(jì)時(shí)。障礙物傳感器UPPAAL Template 如圖5(g)所示。

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

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

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

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

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

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

實(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)換成模型檢測(cè)模型，并對(duì)待檢測(cè)性質(zhì)進(jìn)行檢測(cè)。

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

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

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

新定義局部時(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 信號(hào)到發(fā)出synBlockSensorOutput-Block 信號(hào)的延遲為1～2 個(gè)時(shí)間單位。注入延遲后的障礙物傳感器狀態(tài)機(jī)如圖6(a)所示。

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

新定義局部時(shí)鐘變量tActuatorDelay，用來表達(dá)列車門作動(dòng)器延遲時(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 信號(hào)到輸出開門信號(hào)（actuatorOutput=1）的延遲為1～2 個(gè)時(shí)間單位。注入延遲后列車門作動(dòng)器狀態(tài)機(jī)如圖6(b)所示。利用“增加CF 的經(jīng)更新的系統(tǒng)狀態(tài)機(jī)”生成模型檢測(cè)模型。由于其他狀態(tài)機(jī)保持不變，此處僅展示注入CF 的障礙物傳感器和列車門作動(dòng)器所對(duì)應(yīng)的UPPAAL 模型。注入延遲后列車門作動(dòng)器UPPAAL Template 如圖7(a)所示。注入延遲后障礙物傳感器UPPAAL Template如圖7(b)所示。對(duì)注入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ī)（用于損失場(chǎng)景識(shí)別）Fig.6 SysML state machine after addition of CFs (For identifying loss scenarios)

圖7 增加CF后更新的UPPAAL模型（用于損失場(chǎng)景識(shí)別）Fig.7 UPPAAL model after addition of CFs (For identifying loss scenarios)

違反SpecH2的一條反例（即損失場(chǎng)景）如圖8 所示，其過程如下：

圖8 系統(tǒng)出現(xiàn)H2的一條損失場(chǎng)景Fig.8 A loss scenario leading to H2

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

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

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

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

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

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

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

（8）列車門作動(dòng)器輸出關(guān)門信號(hào)（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 信號(hào)，此時(shí)counter 由start()函數(shù)置0，開始計(jì)時(shí)；

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

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

（13）由于列車門作動(dòng)器輸出開門信號(hào)過程存在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è)損失場(chǎng)景包含了向障礙物傳感器和列車門作動(dòng)器注入的2 個(gè)與信號(hào)傳輸延遲有關(guān)的CF，他們共同作用，在系統(tǒng)的交互運(yùn)行中導(dǎo)致危險(xiǎn)。

4 對(duì)比分析

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

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

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

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

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

5 結(jié) 論

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

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