基于形式化方法的DIMA動態(tài)重構(gòu)仿真與驗證

劉嘉琛, 董 磊,3,*, 趙長嘯,3, 陳泓兵

(1. 中國民航大學(xué)安全科學(xué)與工程學(xué)院, 天津 300300; 2. 中國民航大學(xué)民航航空器適航審定技術(shù)重點實驗室, 天津 300300; 3. 天津市民用航空器適航與維修重點實驗室, 天津 300300)

0 引 言

隨著微電子技術(shù)、信息技術(shù)和高性能計算技術(shù)的迅猛進步,新型航電系統(tǒng)的研發(fā)也得到不斷促進,目前正朝著分布式綜合模塊化航空電子(distributed integrated modular avionics, DIMA)系統(tǒng)的方向發(fā)展。DIMA利用分布式架構(gòu)將聯(lián)合式和模塊化航空電子(integrated modular avio-nics, IMA)的系統(tǒng)理念優(yōu)勢進行結(jié)合,通過高容錯的實時通信網(wǎng)絡(luò)將所有模塊相連,降低了系統(tǒng)和布線的復(fù)雜度。與此同時,歐盟FP7框架下的“可擴展可重配置電子平臺工具”項目指出先進的航電系統(tǒng)中必不可少的一項技術(shù)是具有動態(tài)重構(gòu)能力,這種能力使飛行器可以充分利用功能冗余來進行系統(tǒng)重配置,使其快速適應(yīng)不同飛行任務(wù)模式和資源失效狀態(tài)。因此,動態(tài)重構(gòu)技術(shù)可以減少航電系統(tǒng)對硬件冗余的要求,有效提高了資源的利用率及靈活性。

近年來,國內(nèi)外研究人員針對航電系統(tǒng)的動態(tài)重構(gòu)做了諸多研究。文獻[5]基于動態(tài)重構(gòu)策略及重構(gòu)過程構(gòu)建了面向DIMA系統(tǒng)的聯(lián)合k/n(G)可靠性模型,通過改變功能模塊的不同配置研究其對系統(tǒng)可靠度的影響。文獻[6]提出了一種基于模型的動態(tài)重構(gòu)分析方法,利用架構(gòu)分析與設(shè)計語言(architecture analysis and design language, AADL)建立了動態(tài)重構(gòu)過程模型并將其轉(zhuǎn)化為有色Petri網(wǎng)進行多約束仿真分析,以證明方法的有效性和正確性。文獻[7]提出了一種基于安全性的IMA軟件重構(gòu)方法,利用AADL錯誤模型附件對運行時的體系結(jié)構(gòu)進行了描述,建立了AADL模型到確定性隨機Petri網(wǎng)的映射規(guī)則并驗證了基于安全性的重構(gòu)方法的適用性。文獻[8]提出了一種分布式的可重構(gòu)航電系統(tǒng)體系結(jié)構(gòu),利用AADL語言對平臺、應(yīng)用程序和屬性進行建模,還結(jié)合模型檢驗工具對系統(tǒng)可預(yù)見的情況進行實時性分析。文獻[9]對DIMA系統(tǒng)重構(gòu)實現(xiàn)機制進行了研究,開發(fā)了一種基于DIMA工作流程的調(diào)度程序,并基于動態(tài)重構(gòu)演示了故障恢復(fù)過程。文獻[10]以標準航空電子系統(tǒng)結(jié)構(gòu)聯(lián)合委員會(Allied Standard Avionics Architecture Council, ASAAC)的系統(tǒng)管理為框架和VxWorks653操作系統(tǒng)的健康監(jiān)控機制為基礎(chǔ),設(shè)計并實現(xiàn)了DIMA平臺級和系統(tǒng)級的健康管理方案。文獻[11]提出了一種基于分布式通用系統(tǒng)管理的消息交互機制,滿足了通用系統(tǒng)管理中多節(jié)點、多數(shù)據(jù)流的消息通信需求,有效減少了系統(tǒng)設(shè)計冗余。

可以看出,目前對于DIMA動態(tài)重構(gòu)的研究主要有基于模型的DIMA動態(tài)重構(gòu)可靠性與實時性分析,航電系統(tǒng)體系架構(gòu)的擴展支持以及DIMA動態(tài)重構(gòu)的機制策略方面。這些研究大多將處理模塊內(nèi)部的動態(tài)重構(gòu)功能性組件交互過程視為黑盒,雖然也有針對通用系統(tǒng)管理的研究,但只停留在機制和理論層面,并未涉及具體的形式化建模、仿真及驗證。因此,本文針對可重構(gòu)DIMA系統(tǒng)在設(shè)計初期缺少仿真與驗證手段的問題,使用AADL核心語言及其相關(guān)附件對DIMA動態(tài)重構(gòu)的建模深入到了通用系統(tǒng)管理(generic system management, GSM)功能性組件層級,設(shè)計了基于形式化定義的模型轉(zhuǎn)換規(guī)則,形成可執(zhí)行的時間自動機模型并進行仿真驗證。結(jié)果表明,本文所提的仿真與驗證方法具有可行性和有效性,并且能夠為后續(xù)DIMA動態(tài)重構(gòu)的形式化安全性評估提供模型基礎(chǔ)。

1 可重構(gòu)DIMA系統(tǒng)特性分析

在系統(tǒng)科學(xué)中,系統(tǒng)并不專指某一特定實體或特定事物,國際系統(tǒng)工程協(xié)會對系統(tǒng)給出的定義為:實現(xiàn)一個或多個特定目標的交互元素組合?？芍貥?gòu)DIMA系統(tǒng)包括功能軟件、硬件、接口和相關(guān)功能性組件等元素,可以實現(xiàn)任務(wù)-功能-硬件資源的映射,以便清晰地表達動態(tài)重構(gòu)過程中資源模塊的調(diào)用關(guān)系;本文將環(huán)境定義為航電系統(tǒng)當前的配置狀態(tài),配置狀態(tài)的改變也是動態(tài)重構(gòu)的觸發(fā)條件,此時需要通過重新配置來提高飛機的可靠性、保障其安全性;系統(tǒng)與環(huán)境還以一定的邊界相區(qū)分,可重構(gòu)DIMA系統(tǒng)的邊界參考ASAAC及ARINC653標準中提出的軟件體系架構(gòu),本文與動態(tài)重構(gòu)的相關(guān)研究均在此范圍內(nèi)開展。

1.1 可重構(gòu)DIMA系統(tǒng)映射關(guān)系研究

設(shè)計一個系統(tǒng)時,首先需要對系統(tǒng)的功能進行定義和劃分,然后選擇一個能夠?qū)崿F(xiàn)這些功能的體系結(jié)構(gòu),將功能體系結(jié)構(gòu)映射到系統(tǒng)體系架構(gòu)中,可重構(gòu)DIMA系統(tǒng)的映射關(guān)系包括軟件映射和硬件映射,如圖1所示。

圖1 可重構(gòu)DIMA系統(tǒng)的映射關(guān)系Fig.1 Mapping relationship of reconfigurable DIMA system

DIMA動態(tài)重構(gòu)是系統(tǒng)在靜態(tài)配置基礎(chǔ)上的一種能力延伸,主要體現(xiàn)在系統(tǒng)運行中資源重新配置的能力。這使得航電系統(tǒng)能依據(jù)當前飛行任務(wù)、功能需求和可用資源條件進行合理的配置,實現(xiàn)航電功能對現(xiàn)階段任務(wù)模式的最大化支撐和對飛行安全的保證。由于硬件故障是不可逆的,因此動態(tài)重構(gòu)的本質(zhì)只與軟件有關(guān)。雖然本文也會對執(zhí)行平臺進行建模,但仿真與驗證工作是在其基礎(chǔ)上面向軟件組件展開的。

1.2 可重構(gòu)DIMA系統(tǒng)軟件體系架構(gòu)研究

目前航空領(lǐng)域有兩種典型的DIMA軟件體系架構(gòu),分別來自美國航空無線電技術(shù)委員會提出的ARINC653標準,以及北約聯(lián)合標準航空電子系統(tǒng)結(jié)構(gòu)委員會提出的ASAAC標準,其需要實現(xiàn)的兩個主要目標為:① 搭建可重構(gòu)的軟件框架;② 建立可重用的應(yīng)用程序組件。

經(jīng)對比研究發(fā)現(xiàn),兩種標準提出的軟件體系架構(gòu)趨于一致,但仍有各自的特點。ARINC653標準將架構(gòu)分為應(yīng)用軟件層和核心處理層,核心概念是時空分區(qū)及其協(xié)調(diào)技術(shù),通過APEX接口為應(yīng)用軟件提供實時安全的各類功能服務(wù)。ASAAC標準將架構(gòu)分為應(yīng)用層、操作系統(tǒng)層和模塊支持層,采用4種直接接口和5種邏輯接口實現(xiàn)邏輯通信,通過藍印系統(tǒng)實現(xiàn)調(diào)度控制、配置管理以及健康管理而不是由APEX接口進行控制,還采用了層次化的通用系統(tǒng)管理進一步強化應(yīng)用軟件的功能獨立性?？偟膩碚f,ASAAC軟件體系架構(gòu)更適用于可重構(gòu)DIMA系統(tǒng)的應(yīng)用案例,但在ASAAC標準中分區(qū)的定義和有效范圍跨越了單個處理模塊,這使得ASAAC架構(gòu)在實現(xiàn)方面比ARINC653架構(gòu)更為復(fù)雜。本文結(jié)合以上兩種架構(gòu)的優(yōu)點,給出了一種經(jīng)過優(yōu)化的軟件體系架構(gòu)作為可重構(gòu)DIMA系統(tǒng)邊界,使其同時具備時空分區(qū)與層次化的通用系統(tǒng)管理技術(shù),如圖2所示。

圖2 優(yōu)化的可重構(gòu)DIMA系統(tǒng)軟件體系架構(gòu)Fig.2 Optimized software architecture of reconfigurable DIMA system

1.3 DIMA通用系統(tǒng)管理機制研究

GSM在DIMA軟件體系結(jié)構(gòu)的核心軟件層和應(yīng)用軟件層之間工作,由健康監(jiān)控(health monitor, HM)、故障管理(failure management, FM)、配置管理(configuration management, CM)和安全管理(safety management, SM)4部分組成。GSM是基于NATO STANAG 4626標準的機載系統(tǒng)管理機制,是實現(xiàn)DIMA動態(tài)重構(gòu)不可或缺的重要組成部分。通用系統(tǒng)管理的功能性組件屬于非飛行功能的管理類軟件,功能劃分如表1所示。

表1 GSM組件功能劃分Table 1 Function division of GSM

主動式系統(tǒng)管理會根據(jù)需求變化逐層向下分解實施,如任務(wù)模式改變等。被動式系統(tǒng)管理會根據(jù)狀態(tài)變化逐層上報處理,如系統(tǒng)資源失效等。GSM功能性組件間的消息傳遞包括健康監(jiān)控心跳消息、故障處理信息消息和配置管理動作消息等,相應(yīng)的觸發(fā)動作在藍印系統(tǒng)中定義以供調(diào)用,工作流程如圖3所示。

圖3 GSM的層次化工作流程Fig.3 GSM hierarchical workflow of GSM

2 可重構(gòu)DIMA系統(tǒng)的AADL建模方法

2.1 AADL概述

AADL是由美國汽車工程師協(xié)會于2004年提出的一種面向安全關(guān)鍵系統(tǒng)的建模語言標準,即AS5506標準。AADL模型主要由組件類型、組件實現(xiàn)和屬性集等元素構(gòu)成,支持對軟件、硬件和系統(tǒng)3個層次的文本或者圖形化建模,旨在實現(xiàn)基于航空標準的嵌入式系統(tǒng)模型的開發(fā)工作。AADL在軟件體系結(jié)構(gòu)上通過線程、進程、子程序等組件以及組件交互進行描述;在硬件體系結(jié)構(gòu)上通過處理器、虛擬處理器和總線等組件以及組件交互進行描述;功能和非功能屬性通過通信協(xié)議、模式變換協(xié)議以及分區(qū)機制等屬性進行描述;最后,通過系統(tǒng)組件的組合,能夠?qū)哟位亟⑵鹣到y(tǒng)的體系結(jié)構(gòu)模型。本文使用開源工具環(huán)境OSATE(open source AADL tool environment)進行建模,此工具由軟件工程師協(xié)會開發(fā)的基于Eclipse平臺的AADL模型建模和分析工具,支持以文本和圖形的方式建立并編輯AADL模型。

此外,AADL還支持語義擴展,在AS5506標準的基礎(chǔ)上相繼頒布了ARINC653 Annex、Behavior ModelAnnex和Error Model Annex等附件,進一步擴展了AADL語言的描述能力,使其更適合具體的建模需求。

2.2 DIMA動態(tài)重構(gòu)的AADL模型

根據(jù)前述對可重構(gòu)DIMA系統(tǒng)特性和AADL建模工具的分析,建立DIMA動態(tài)重構(gòu)到AADL實體的映射規(guī)則如表2所示。通過AADL核心語言以及ARINC653 Annex對這些AADL實體進行建模,用虛擬處理器為子組件的處理器表示動態(tài)重構(gòu)中的通用功能模塊(common function model, CFM);用綁定到虛擬處理器的進程表示分區(qū);用線程表示功能應(yīng)用和與動態(tài)重構(gòu)相關(guān)的功能性組件以及分區(qū)中的功能應(yīng)用;用端口和端口之間的連接表示模塊間和應(yīng)用間的交互;用數(shù)據(jù)表示DIMA動態(tài)重構(gòu)策略中各功能應(yīng)用的資源要求、與其他應(yīng)用的通訊配置、故障處理動作等信息;再以綁定語法實現(xiàn)系統(tǒng)的軟硬件物理資源分配關(guān)系,建立可重構(gòu)的DIMA架構(gòu)模型;接下來,通過Behavior Model-Annex定義一個狀態(tài)遷移模型以表征重構(gòu)過程的遷移和動作,包含變量聲明、狀態(tài)聲明和轉(zhuǎn)換聲明;將其與模態(tài)結(jié)合,表示通用功能模塊在重構(gòu)過程的不同配置狀態(tài)。DIMA動態(tài)重構(gòu)模型用AADL圖形化的方式表達如圖4和圖5所示。

表2 DIMA動態(tài)重構(gòu)到AADL實體的映射規(guī)則Table 2 Mapping rules from DIMA dynamic reconfiguration to AADL entities

圖4 AADL圖形化表示的系統(tǒng)級動態(tài)重構(gòu)模型Fig.4 System level dynamic reconfiguration model based on AADL graphical representation

圖5 AADL圖形化表示的模塊級動態(tài)重構(gòu)模型Fig.5 Module level dynamic reconfiguration model based on AADL graphical representation

需要注意的是,AADL模型中變量選擇的依據(jù)是系統(tǒng)理論過程分析(systematic theory process analysis, STPA),此方法不再關(guān)注組件的故障或可靠性目標是否達到要求,而是在識別不安全控制行為的基礎(chǔ)上將安全問題轉(zhuǎn)化為控制問題,更注重系統(tǒng)本身的特點以及多方交互的非線性影響。本文將從3個方面歸納動態(tài)重構(gòu)組件控制行為中可能存在的安全隱患,對應(yīng)的變量值分別為{1,2,3}:① 未提供控制行為導(dǎo)致危險;② 提供錯誤的控制行為導(dǎo)致危險;③ 提供可能安全的控制行為但提供節(jié)點過早、過晚或順序錯誤;④ 控制行為持續(xù)太久或過早停止(僅針對持續(xù)性控制行為而非離散行為,本文不予考慮)。

2.3 針對動態(tài)重構(gòu)的AADL形式化定義

AADL雖然有確定的語義和嚴格的語法表達規(guī)范,但不可執(zhí)行性決定了其無法直接仿真模型以評估系統(tǒng)特性。因此,學(xué)術(shù)界傾向于使用模型轉(zhuǎn)換方法,利用現(xiàn)有的形式化理論或工具間接分析AADL模型。由于本文的目的是通過模型轉(zhuǎn)換生成可執(zhí)行的DIMA動態(tài)重構(gòu)目標模型,因此源模型的主要關(guān)注點為線程和行為模型附件,這兩部分的元素已經(jīng)可以充分表達動態(tài)重構(gòu)過程中的組件交互關(guān)系,其形式化定義如下。

AADL線程組件可以定義為一個五元組Th=〈,, Disp, BA, Con〉其中:

(1)={eventport, dataport, eventport}是綁定線程的數(shù)據(jù)接口、事件端口和數(shù)據(jù)事件端口的集合;

(2)={×, La}是線程內(nèi)部數(shù)據(jù)流flow的表示,La是時延屬性Latency的集合,以端口到端口以及轉(zhuǎn)移過程中的時延定義;

(3) Disp表示線程的調(diào)度策略,其主要屬性有Period、Compute_Execution_Time、Priority等。其中Period為時鐘周期,本文默認截止時鐘為周期值;

(4) BA表示線程的具體行為,即行為模型;

(5) Con={×,}是線程間端口連接connection的集合,為連接的約束條件。

AADL行為模型附件可以定義為一個六元組BA=〈,,,,,〉,其中:

(1)是狀態(tài)集合。狀態(tài)有多種類型,如Initial表示初始狀態(tài),Complete表示完成狀態(tài),Final表示最終狀態(tài),Complete表示該狀態(tài)可以是一個組合狀態(tài);

(2)∈是初始狀態(tài)的有限集合;

(3)是局部變量的集合,一般為行為附件使用的輔助變量;

(4)是狀態(tài)轉(zhuǎn)換的使能條件,針對狀態(tài)變量進行邏輯判斷,確定是否進行狀態(tài)轉(zhuǎn)換;

(5)是狀態(tài)轉(zhuǎn)換需要執(zhí)行的動作,包括發(fā)送數(shù)據(jù),計算等;

3 DIMA動態(tài)重構(gòu)模型轉(zhuǎn)換及仿真驗證方法

3.1 時間自動機概述及形式化定義

由于可重構(gòu)DIMA系統(tǒng)功能性組件交互復(fù)雜,且具有周期性、有界響應(yīng)等與時間相關(guān)的系統(tǒng)行為特征。為了研究可重構(gòu)DIMA系統(tǒng)狀態(tài)之間的遷移需要滿足的時鐘約束,本文選擇時間自動機作為目標模型。時間自動機理論是在有限狀態(tài)自動機的基礎(chǔ)上擴充時鐘、時鐘約束和不變條件而得到的,自提出后便一直廣泛應(yīng)用于描述實時系統(tǒng),有助于對系統(tǒng)體系結(jié)構(gòu)進行分析與驗證。UPPAAL是一種基于時間自動機的形式化驗證工具,可以通過編輯器、模擬器和驗證器構(gòu)造時間自動機網(wǎng)絡(luò)模型對實時系統(tǒng)進行建模、仿真和驗證。不僅能描述動態(tài)重構(gòu)行為的連續(xù)時間特性,還可以體現(xiàn)系統(tǒng)多方交互的特點,實現(xiàn)對可重構(gòu)DIMA系統(tǒng)特性的模擬與驗證。時間自動機的形式化定義如下。

一個時間自動機可以定義為一個六元組TA=〈,,, Var,,〉,其中:

(1)是時間自動機中所有位置(狀態(tài))的非空集合;

(2)∈是時間自動機的初始狀態(tài);

(3)={clock}是有窮的時鐘集合,時鐘默認從0開始,每次自增1,且可以在任意時刻被復(fù)位為0;

(4) Var是一系列變量的集合;

(5)?×Gu×Act××是位置變遷的集合。Gu表示一個使能條件的集合。Act表示輸入(記為？)和輸出(記為！)的同步信號。是對時鐘變量或整型變量的更新操作,在狀態(tài)變遷的同時完成變量的賦值;

(6)是不變條件,是狀態(tài)轉(zhuǎn)移約束函數(shù)的集合。

時間自動機網(wǎng)絡(luò)可以定義為一個四元組NTA=〈TA,Var,, Ch〉,其中:

(1) TA=〈TA,TA,…,TA〉是一組相互平行且相互關(guān)聯(lián)的時間自動機;

(2) Var是一系列共享(全局)變量的集合;

(3)是全局時鐘的集合;

(4) Ch是同步信道的集合。

3.2 AADL到UPPAAL的模型轉(zhuǎn)換規(guī)則設(shè)計

不同的模型轉(zhuǎn)換具有不一樣的評價標準,尋求統(tǒng)一的向?qū)揭?guī)則以供選擇最佳的模型轉(zhuǎn)換方式顯然是不現(xiàn)實的,但可以借鑒軟件工程中的一些基本評價標準。本文擬解決可重構(gòu)DIMA系統(tǒng)在設(shè)計初期缺少安全性評估手段的問題,因此模型轉(zhuǎn)換的主要評價手段是目標模型的行為可達性、邏輯正確性以及模型轉(zhuǎn)換的完整性。兩種模型的形式化的語義已在上文明確定義,接下來將具體闡述語義映射的轉(zhuǎn)換規(guī)則。

3.2.1 AADL線程到時間自動機的映射

Th→TA/TA對于AADL的每一個線程實現(xiàn),都轉(zhuǎn)換為一個單獨的時間自動機,即UPPAAL中的模板。

La→〈〉對應(yīng)于時間自動機的時鐘變量,可以設(shè)置組件內(nèi)部數(shù)據(jù)流中幾個分段的時延(或整個流的總時延)。

〈,Disp〉→〈(Gu,),〉每個線程內(nèi)部數(shù)據(jù)流的時延轉(zhuǎn)換有時鐘賦值、不變條件和轉(zhuǎn)移條件3個部分,其中時鐘賦值包括時鐘clock的重置與變量值的更新,在端口對應(yīng)狀態(tài)的進入條件鐘設(shè)置,其時鐘設(shè)置為0。

不變條件表示當前位置下恒滿足的時鐘約束,映射到流延遲屬性是線程的最大處理時間,即clock≤max{Compute_Execution_Time}。

轉(zhuǎn)移條件是模板內(nèi)位置間的轉(zhuǎn)移約束,通常是時鐘范圍以及共享全局變量的要求,映射到流延遲屬性中是數(shù)據(jù)流的延遲,即clock==Latency。

3.2.2 行為模型附件到時間自動機的映射

〈,〉→〈,〉,時間自動機中以位置表示狀態(tài)的存在,因此本文將行為模型中的狀態(tài)聲明映射為時間自動機中的位置。同時,行為模型中初始狀態(tài)作為線程調(diào)度執(zhí)行的最初狀態(tài),與對應(yīng)時間自動機模板中的初始位置相對應(yīng),完成狀態(tài)和最終狀態(tài)表示線程行為變化的結(jié)束。

〈Con,〉→〈Var/Var, Ch〉將AADL行為模型中的變量映射為時間自動機變量Var的集合,端口輸出的變量值可以映射為同步信道Ch的集合,Con規(guī)定了端口連接的方向。

〈,〉→(Act,)AADL行為附件狀態(tài)遷移過程的動作對應(yīng)于時間自動機位置變遷過程發(fā)生的動作Act,分為一般動作、端口動作和延時動作3類。一般動作包括變量的賦值和子程序調(diào)用,本文將其映射為時間自動機位置變遷過程中的變量更新;端口動作表示線程通過端口輸出事件或變量值;延時動作包含delay和computation兩種,本文采取computation(clock)表達此動作消耗的計算時間,可以將其作為時間自動機位置遷移的使能條件之一。

3.2.3 基本數(shù)據(jù)類型的映射

AADL標準語義中已經(jīng)定義了基本數(shù)據(jù)類型的package,包括布爾型(boolean)、實型(float)和整型(integer)。時間自動機建模工具UPPAAL的變量聲明中主要包含布爾型(bool)、整型(int)、數(shù)組類型(array)和結(jié)構(gòu)數(shù)據(jù)類型(struct)，其映射關(guān)系如表3所示。

表3 數(shù)據(jù)類型映射關(guān)系Table 3 Mapping of data types

3.3 DIMA動態(tài)重構(gòu)的時間自動機模型

根據(jù)前述的模型轉(zhuǎn)換規(guī)則,可以將第2節(jié)建立的AADL動態(tài)重構(gòu)模型中的線程和行為模型附件轉(zhuǎn)換為基于UPPAAL的時間自動機模型,如圖6所示。時間自動機模型使用AADL模型中定義的變量來區(qū)分功能狀態(tài),例如變量“XXX_s”表示當前線程的工作狀態(tài),取值范圍{1,2,3}={正確執(zhí)行,錯誤執(zhí)行,未執(zhí)行};變量“XXX_o”表示當前線程的輸出狀態(tài),輸入變量為上一個模塊的輸出變量,取值范圍{1,2,3}={正確輸出,錯誤輸出,無輸出};“XXX_F()”為過程模型函數(shù),表示變量之間的變化關(guān)系,其中“XXX”為對應(yīng)線程狀態(tài)/位置的名稱。

圖6 基于時間自動機的DIMA動態(tài)重構(gòu)模型Fig.6 DIMA dynamic reconfiguration model based on timed automata

3.4 時間自動機模型的仿真驗證

模型轉(zhuǎn)換工作完成后,利用UPPAAL工具中的模擬器對DIMA動態(tài)重構(gòu)過程進行模擬仿真,生成的DIMA動態(tài)重構(gòu)序列圖遵循圖3中通用系統(tǒng)管理在功能分區(qū)層級的工作流程,表明了模型語義轉(zhuǎn)換的正確性。DIMA動態(tài)重構(gòu)模擬仿真示例如圖7所示。再利用巴科斯范式(backus-naur form, BNF)語句對模型需要驗證的性質(zhì)進行描述和驗證,BNF是用來描述語法的一種形式體系,是一種典型的元語言,能夠嚴格地表示語法規(guī)則,驗證語句的含義如表4所示。

圖7 DIMA動態(tài)重構(gòu)模擬仿真示例(部分)Fig.7 Example of DIMA dynamic reconfiguration simulation (portion)

表4 BNF驗證語句含義

首先驗證的是目標模型的系統(tǒng)邏輯和時序正確性,若性質(zhì)滿足則說明GSM各功能性組件均能正常執(zhí)行,驗證結(jié)果如表5所示。

接下來,利用BNF語句驗證是否存在一條轉(zhuǎn)移路徑使得不安全控制行為發(fā)生,若性質(zhì)滿足,說明控制行為會發(fā)生,反之亦然,以此判斷不安全控制行為(unsafe control action, UCA)故障轉(zhuǎn)移路徑的可達性。下面以配置管理部分的“加載新配置”功能為例,使用STPA方法識別出了5條不安全控制行為,對其行為可達性進行驗證后發(fā)現(xiàn)UCA5不滿足可達性要求,即此類不安全控制行為不會發(fā)生。針對UCA的可達性驗證也是對需求的驗證,屬于安全性工作的一部分,表明了本文的時間自動機DIMA動態(tài)重構(gòu)模型進行STPA安全性分析的可行性,驗證結(jié)果如表6所示。

表5 系統(tǒng)邏輯及時序正確性驗證Table 5 Verification of system logic and time sequence correctness

表6 動態(tài)重構(gòu)行為可達性驗證Table 6 Reachability verification of dynamic reconfiguration behavior

4 結(jié) 論

本文在分析可重構(gòu)DIMA軟件體系的架構(gòu)特征及層次化通用系統(tǒng)管理組件功能劃分的基礎(chǔ)上,利用AADL核心語言、ARINC653附件以及行為模型附件對可重構(gòu)DIMA系統(tǒng)的架構(gòu)和動態(tài)重構(gòu)行為進行建模,通過一種形式化的模型轉(zhuǎn)換規(guī)則生成了可執(zhí)行仿真的動態(tài)重構(gòu)時間自動機模型,對目標模型的邏輯及時序正確性和行為可達性的驗證結(jié)果表明,本文所提方法針對DIMA系統(tǒng)設(shè)計初期的模型仿真與驗證是可行且有效的。后續(xù)研究可將AADL錯誤模型附件加入到本文所建模型中,進一步展開STPA安全性分析和可靠性分析,對于復(fù)雜航電系統(tǒng)的安全性發(fā)展具有重要意義。