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

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

0 引 言

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

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

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

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

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

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

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

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

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

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

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標(biāo)準(zhǔn)的機(jī)載系統(tǒng)管理機(jī)制,是實(shí)現(xiàn)DIMA動(dòng)態(tài)重構(gòu)不可或缺的重要組成部分。通用系統(tǒng)管理的功能性組件屬于非飛行功能的管理類軟件,功能劃分如表1所示。

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

主動(dòng)式系統(tǒng)管理會(huì)根據(jù)需求變化逐層向下分解實(shí)施,如任務(wù)模式改變等。被動(dòng)式系統(tǒng)管理會(huì)根據(jù)狀態(tài)變化逐層上報(bào)處理,如系統(tǒng)資源失效等。GSM功能性組件間的消息傳遞包括健康監(jiān)控心跳消息、故障處理信息消息和配置管理動(dòng)作消息等,相應(yīng)的觸發(fā)動(dòng)作在藍(lán)印系統(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é)會(huì)于2004年提出的一種面向安全關(guān)鍵系統(tǒng)的建模語言標(biāo)準(zhǔn),即AS5506標(biāo)準(zhǔn)。AADL模型主要由組件類型、組件實(shí)現(xiàn)和屬性集等元素構(gòu)成,支持對(duì)軟件、硬件和系統(tǒng)3個(gè)層次的文本或者圖形化建模,旨在實(shí)現(xiàn)基于航空標(biāo)準(zhǔn)的嵌入式系統(tǒng)模型的開發(fā)工作。AADL在軟件體系結(jié)構(gòu)上通過線程、進(jìn)程、子程序等組件以及組件交互進(jìn)行描述;在硬件體系結(jié)構(gòu)上通過處理器、虛擬處理器和總線等組件以及組件交互進(jìn)行描述;功能和非功能屬性通過通信協(xié)議、模式變換協(xié)議以及分區(qū)機(jī)制等屬性進(jìn)行描述;最后,通過系統(tǒng)組件的組合,能夠?qū)哟位亟⑵鹣到y(tǒng)的體系結(jié)構(gòu)模型。本文使用開源工具環(huán)境OSATE(open source AADL tool environment)進(jìn)行建模,此工具由軟件工程師協(xié)會(huì)開發(fā)的基于Eclipse平臺(tái)的AADL模型建模和分析工具,支持以文本和圖形的方式建立并編輯AADL模型。

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

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

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

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

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

圖5 AADL圖形化表示的模塊級(jí)動(dòng)態(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)注組件的故障或可靠性目標(biāo)是否達(dá)到要求,而是在識(shí)別不安全控制行為的基礎(chǔ)上將安全問題轉(zhuǎn)化為控制問題,更注重系統(tǒng)本身的特點(diǎn)以及多方交互的非線性影響。本文將從3個(gè)方面歸納動(dòng)態(tài)重構(gòu)組件控制行為中可能存在的安全隱患,對(duì)應(yīng)的變量值分別為{1,2,3}:① 未提供控制行為導(dǎo)致危險(xiǎn);② 提供錯(cuò)誤的控制行為導(dǎo)致危險(xiǎn);③ 提供可能安全的控制行為但提供節(jié)點(diǎn)過早、過晚或順序錯(cuò)誤;④ 控制行為持續(xù)太久或過早停止(僅針對(duì)持續(xù)性控制行為而非離散行為,本文不予考慮)。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1 時(shí)間自動(dòng)機(jī)概述及形式化定義

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

一個(gè)時(shí)間自動(dòng)機(jī)可以定義為一個(gè)六元組TA=〈,,, Var,,〉,其中:

(1)是時(shí)間自動(dòng)機(jī)中所有位置(狀態(tài))的非空集合;

(2)∈是時(shí)間自動(dòng)機(jī)的初始狀態(tài);

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

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

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

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

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

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

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

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

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

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

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

3.2.1 AADL線程到時(shí)間自動(dòng)機(jī)的映射

Th→TA/TA對(duì)于AADL的每一個(gè)線程實(shí)現(xiàn),都轉(zhuǎn)換為一個(gè)單獨(dú)的時(shí)間自動(dòng)機(jī),即UPPAAL中的模板。

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

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

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

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

3.2.2 行為模型附件到時(shí)間自動(dòng)機(jī)的映射

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

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

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

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

AADL標(biāo)準(zhǔn)語義中已經(jīng)定義了基本數(shù)據(jù)類型的package,包括布爾型(boolean)、實(shí)型(float)和整型(integer)。時(shí)間自動(dòng)機(jī)建模工具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動(dòng)態(tài)重構(gòu)的時(shí)間自動(dòng)機(jī)模型

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

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

3.4 時(shí)間自動(dòng)機(jī)模型的仿真驗(yàn)證

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

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

表4 BNF驗(yàn)證語句含義

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

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

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

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

4 結(jié) 論

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