許金淼，楊志斌,2，黃志球,2+，謝 健,2，周 勇,2

1.南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京210016

2.高安全系統(tǒng)的軟件開發(fā)與驗(yàn)證技術(shù)工信部重點(diǎn)實(shí)驗(yàn)室，南京210016

+通訊作者E-mail:zqhuang@nuaa.edu.cn

1 引言

嵌入式系統(tǒng)廣泛應(yīng)用于航空、航天、核能等領(lǐng)域，這些系統(tǒng)具有資源受限、交互頻繁等特點(diǎn)，對(duì)實(shí)時(shí)性、可靠性等性質(zhì)有非常高的要求，因此也稱為安全關(guān)鍵系統(tǒng)（safety-critical systems）。由于功能和非功能要求不斷提高，系統(tǒng)的復(fù)雜度急劇增加。如何設(shè)計(jì)與實(shí)現(xiàn)高質(zhì)量的安全關(guān)鍵嵌入式系統(tǒng)，并有效控制開發(fā)時(shí)間和成本，是學(xué)術(shù)界和工業(yè)界共同面臨的難題。近年來(lái)，模型驅(qū)動(dòng)開發(fā)方法（model-driven development，MDD）逐漸成為安全關(guān)鍵系統(tǒng)設(shè)計(jì)與開發(fā)的重要手段[1]。

MDD 作為一種軟件系統(tǒng)開發(fā)的綜合方法，它以UML（unified modeling language）及相關(guān)技術(shù)和實(shí)踐為基礎(chǔ)。MDD的中心概念之一是模型細(xì)分為平臺(tái)無(wú)關(guān)模型（platform independent model，PIM）和平臺(tái)相關(guān)模型（platform specific model，PSM）?，F(xiàn)階段，工業(yè)界常用的建模語(yǔ)言包括UML、SysML 和AADL（architecture analysis and design language）等。UML 是一種支持模型化和軟件系統(tǒng)開發(fā)的圖形語(yǔ)言。它可以通過(guò)類圖對(duì)數(shù)據(jù)建模，通過(guò)狀態(tài)圖對(duì)行為建模，通過(guò)活動(dòng)圖、序列圖對(duì)組件之間的交互建模。UML 支持軟件的開發(fā)過(guò)程，可以建模平臺(tái)無(wú)關(guān)模型（PIM）。但是，對(duì)于安全關(guān)鍵嵌入式系統(tǒng)，運(yùn)行時(shí)間等非功能屬性尤為重要。這些非功能屬性依賴于執(zhí)行平臺(tái)信息，而UML是一種通用的建模語(yǔ)言，在表達(dá)安全關(guān)鍵嵌入式系統(tǒng)特有的某些非功能屬性時(shí)不夠精確[2]。SysML 是一種用于規(guī)范、分析、設(shè)計(jì)復(fù)雜系統(tǒng)（包括軟硬件信息）的通用圖形建模語(yǔ)言。SysML 是對(duì)UML2.0子集的重用和擴(kuò)充，它的需求圖支持結(jié)構(gòu)化的需求建模且可以提高可追溯性，參數(shù)圖可以捕捉物理系統(tǒng)的動(dòng)態(tài)特征。但SysML 關(guān)注于系統(tǒng)層建模，不擅于表達(dá)計(jì)算機(jī)運(yùn)行時(shí)環(huán)境（包括線程、進(jìn)程，以及對(duì)處理器的分配）等特性[2]。另外，SysML 缺少精確的形式化語(yǔ)義描述，不利于后期的形式化驗(yàn)證。而AADL[3-4]是一種復(fù)雜嵌入式系統(tǒng)架構(gòu)描述語(yǔ)言，它通過(guò)組件的概念描述嵌入式軟硬件系統(tǒng)。AADL提供線程、線程組和進(jìn)程來(lái)表示在受保護(hù)的地址空間（時(shí)間和空間分區(qū)）中執(zhí)行的并發(fā)任務(wù)，通過(guò)端口、共享數(shù)據(jù)組件和服務(wù)調(diào)用來(lái)表示軟件運(yùn)行時(shí)體系結(jié)構(gòu)。此外，AADL 標(biāo)準(zhǔn)為任務(wù)執(zhí)行、通信時(shí)序以及模式轉(zhuǎn)換提供了精確的執(zhí)行語(yǔ)義，也稱之為AADL執(zhí)行模型[5]。

嵌入式系統(tǒng)的功能行為建模包括控制流建模與數(shù)據(jù)流建模。如圖1所示，給出了AADL功能行為建模擴(kuò)展的總體框架，包括基于行為附件對(duì)控制流功能行為建模以及基于同步語(yǔ)言SIGNAL[6]對(duì)數(shù)據(jù)流功能行為建模。

Fig.1 Global view of AADL functional modeling圖1 AADL功能行為建?？傮w框架

為了支持組件內(nèi)部的控制流建模，法國(guó)IRIT實(shí)驗(yàn)室于2006年提出了AADL行為附件（behavior annex）[7]。行為附件以變遷系統(tǒng)（transition system）的形式增強(qiáng)了AADL線程構(gòu)件和子程序構(gòu)件功能行為的詳細(xì)描述能力[8]。行為附件與執(zhí)行模型有密切的關(guān)系：執(zhí)行模型定義行為附件何時(shí)執(zhí)行，哪些數(shù)據(jù)被改變，而行為附件處于構(gòu)件內(nèi)部，對(duì)線程、子程序構(gòu)件的執(zhí)行給予更精確的描述[9]。

在對(duì)工業(yè)實(shí)際案例建模過(guò)程中，可能存在如下問(wèn)題：（1）建模實(shí)際的工業(yè)項(xiàng)目是一個(gè)不斷精化的過(guò)程，扁平化的狀態(tài)機(jī)難以適應(yīng)頻繁的精化。（2）工業(yè)界的實(shí)際項(xiàng)目中有許多復(fù)雜的多層嵌套的層次狀態(tài)機(jī)。如果這些嵌套狀態(tài)機(jī)被展開，將會(huì)形成一個(gè)巨大且難以管理的狀態(tài)機(jī)圖。（3）扁平化模型難以管理大量的組件，并且扁平化模型會(huì)造成結(jié)構(gòu)信息的丟失。因此，對(duì)于AADL行為附件來(lái)說(shuō)，層次化地表達(dá)功能行為是一個(gè)非常重要的特征。

為了解決扁平狀態(tài)機(jī)的問(wèn)題，Elattar等人擴(kuò)展了UML 狀態(tài)圖Statecharts[10]。相應(yīng)地，David 提出了層次時(shí)間狀態(tài)機(jī)（hierarchical timed automata，HTA）[11]的概念，用于解決UPPAAL 中的層次化建模問(wèn)題。另外，F(xiàn)ran?a 等人[12]通過(guò)對(duì)飛行控制軟件的實(shí)際建模，評(píng)估了AADL 行為附件，提出了在AADL 行為附件中引入層次化概念的想法。然而，他們沒有給出形式化的語(yǔ)法、語(yǔ)義定義以及層次化擴(kuò)展的實(shí)現(xiàn)。

在本文中，根據(jù)層次化控制流建模思想，提出了AADL行為附件的層次擴(kuò)展，命名為HBA（hierarchical behavior annex）。然后，給出了HBA 的形式語(yǔ)法和語(yǔ)義定義。為了實(shí)現(xiàn)HBA，給出了AADL 行為附件的元模型擴(kuò)展。此外，完整的HBA 插件已被集成到AADL開源環(huán)境OSATE（open source AADL tool environment）中。為了便于形式化驗(yàn)證，給出了HBA到時(shí)間自動(dòng)機(jī)TA（time automata）的轉(zhuǎn)換規(guī)則，并利用UPPAAL工具對(duì)模型性質(zhì)進(jìn)行分析。最后，介紹一個(gè)使用HBA的實(shí)際工業(yè)案例。

本文的其余部分結(jié)構(gòu)如下：第2章介紹了AADL和行為附件；第3 章給出了HBA 的語(yǔ)法定義；第4 章定義了HBA 的形式語(yǔ)義；第5 章介紹了AADL 行為附件層次化擴(kuò)展的實(shí)現(xiàn)；第6 章給出了HBA 到TA（timed automata）的轉(zhuǎn)換規(guī)則；第7章介紹了一個(gè)實(shí)際的工業(yè)案例研究；第8 章討論相關(guān)工作；第9 章給出結(jié)論。

2 研究背景

2.1 AADL語(yǔ)言簡(jiǎn)介

AADL 是一種專為嵌入式系統(tǒng)建模而設(shè)計(jì)的架構(gòu)描述語(yǔ)言。它支持高度可演化系統(tǒng)的開發(fā)，系統(tǒng)架構(gòu)的早期分析，以及用于整個(gè)生命周期持續(xù)分析的架構(gòu)模型的演變。

AADL采用半形式化的建模概念，描述了復(fù)雜嵌入式系統(tǒng)的軟件、硬件架構(gòu)和非功能屬性，包括不同的組件及其交互。AADL 提供了一組預(yù)定義的組件類別[3-4]：

（1）線程、線程組、子程序、數(shù)據(jù)、進(jìn)程。

（2）處理器、內(nèi)存、總線、外設(shè)。

（3）用系統(tǒng)表示軟件和執(zhí)行平臺(tái)的組合集。

例如，一個(gè)線程表示一個(gè)連續(xù)的執(zhí)行流程，它是唯一可以被調(diào)度的AADL組件。一個(gè)子程序表示一段可以被線程或另一個(gè)子程序調(diào)用的代碼。

組件之間的通信可以通過(guò)數(shù)據(jù)流、子程序調(diào)用或訪問(wèn)共享變量來(lái)實(shí)現(xiàn)。這些不同的通信方式在通信組件的接口中聲明。根據(jù)所選擇的通信方式實(shí)例，通信連接點(diǎn)可能是端口（port）、子程序（subprogram）或數(shù)據(jù)訪問(wèn)（data access）[8]。

系統(tǒng)行為不僅依賴于上述組件及其連接所定義的體系結(jié)構(gòu)，還依賴于運(yùn)行時(shí)環(huán)境[13]。AADL標(biāo)準(zhǔn)將執(zhí)行模型指定為虛擬運(yùn)行時(shí)環(huán)境（包含同步和異步模式），以支持組件的執(zhí)行和管理。在執(zhí)行模型中也定義了諸如截止日期、調(diào)度時(shí)間等時(shí)間屬性，這些屬性通過(guò)AADL屬性聲明。

此外，AADL 支持兩種擴(kuò)展方式：屬性集和附件。屬性集擴(kuò)展允許用戶引入新的屬性集。例如，調(diào)度分析工具Cheddar，通過(guò)定義新的屬性集增強(qiáng)了AADL支持更復(fù)雜調(diào)度算法的能力?，F(xiàn)有的附件包括AADL錯(cuò)誤模型附件[14]、AADL行為附件[7]、ARINC653附件、數(shù)據(jù)模型附件等。

2.2 AADL行為附件

行為附件是執(zhí)行模型調(diào)度機(jī)制的擴(kuò)展，用于更精確地描述模型行為，例如端口通信、子程序調(diào)用、時(shí)序、異步等。AADL執(zhí)行模型指定行為附件何時(shí)執(zhí)行，并指定哪些數(shù)據(jù)被執(zhí)行。完整的AADL 模型應(yīng)該包括執(zhí)行模型和行為附件。現(xiàn)在行為附件可以附加到AADL 的任何組件中。它通過(guò)擴(kuò)展的AADL 模式自動(dòng)機(jī)[7]來(lái)描述組件行為，例如：“initial”指定自動(dòng)機(jī)的初始狀態(tài)，“complete”指定線程完成，轉(zhuǎn)換可以包括條件和動(dòng)作，條件和動(dòng)作包括發(fā)送或接收事件，調(diào)用或執(zhí)行子程序等。

行為附件主要包括三部分：變量、狀態(tài)和轉(zhuǎn)換。變量部分聲明當(dāng)前行為附件中使用的所有局部變量。局部變量可以用來(lái)保存當(dāng)前行為附件范圍內(nèi)的中間結(jié)果。狀態(tài)部分枚舉狀態(tài)機(jī)的所有狀態(tài)及其屬性（initial，complete，final 或它們的組合）。默認(rèn)狀態(tài)是一個(gè)執(zhí)行狀態(tài)。轉(zhuǎn)換定義了從源狀態(tài)到目標(biāo)狀態(tài)的轉(zhuǎn)換，轉(zhuǎn)換可以有條件和動(dòng)作。

下面給出一個(gè)線程的行為附件的示例代碼：

3 層次行為附件（HBA）語(yǔ)法

HBA擴(kuò)展了AADL行為附件以增強(qiáng)行為附件的層次描述能力。HBA 保留AADL 行為附件的變量、狀態(tài)和轉(zhuǎn)換，添加層次映射函數(shù)和復(fù)合狀態(tài)。

定義1（層次行為附件HBA）層次行為附件是一個(gè)六元組＜Var,S,S0,η,T,type＞，其中：

Var是自動(dòng)機(jī)中使用的局部變量的有限集合。S是一個(gè)非空有限的狀態(tài)集合。S0?S是初始狀態(tài)的有限集合。η:S→2S是層次函數(shù)，它將S映射到S的所有可達(dá)的子狀態(tài)上。映射η將會(huì)產(chǎn)生一個(gè)根節(jié)點(diǎn)為root的樹結(jié)構(gòu)，其中root∈S。通過(guò)η來(lái)記錄某狀態(tài)S與其子狀態(tài)的層次關(guān)系。type窮舉了所有狀態(tài)的類型。復(fù)合狀態(tài)是AND 或者XOR 類型。非復(fù)合狀態(tài)是基本狀態(tài)（BASIC）、入口狀態(tài)（ENTRY）、出口狀態(tài)（EXIT）或歷史狀態(tài)（HISTORY）中的一種。

AND狀態(tài)表示該復(fù)合狀態(tài)的所有子狀態(tài)是并發(fā)執(zhí)行的，即當(dāng)父狀態(tài)被執(zhí)行時(shí)，其內(nèi)部各子狀態(tài)同時(shí)從各自的初始狀態(tài)開始執(zhí)行。在后續(xù)的HBA 實(shí)現(xiàn)中，將AND 狀態(tài)表示為“concurrent state”。XOR 表示該復(fù)合狀態(tài)內(nèi)的所有子狀態(tài)是互斥執(zhí)行，即同一時(shí)刻有且僅有一個(gè)子狀態(tài)被執(zhí)行。在后續(xù)的HBA實(shí)現(xiàn)中，將AND狀態(tài)表示為“composite state”。ENTRY狀態(tài)表示該非復(fù)合狀態(tài)是其父狀態(tài)的入口狀態(tài)，即當(dāng)進(jìn)入其父狀態(tài)時(shí)，默認(rèn)進(jìn)入該子狀態(tài)。EXIT 狀態(tài)表示該非復(fù)合狀態(tài)為出口狀態(tài)，即將要從其父狀態(tài)轉(zhuǎn)移到下一狀態(tài)時(shí)，由該狀態(tài)轉(zhuǎn)移至下一狀態(tài)。HISTORY 狀態(tài)是一個(gè)偽狀態(tài)，其目的是記住從組合狀態(tài)中退出時(shí)所處的子狀態(tài)，當(dāng)再次進(jìn)入組合狀態(tài)時(shí)，可直接進(jìn)入這個(gè)子狀態(tài)，而不是再次從組合狀態(tài)的ENTRY狀態(tài)開始。

T?s×(Guard×Action)×s是轉(zhuǎn)換函數(shù)。一個(gè)轉(zhuǎn)換連接兩個(gè)狀態(tài)S和S′，轉(zhuǎn)換有一個(gè)條件guard，或?yàn)椴紶栔?。轉(zhuǎn)換完成時(shí)可執(zhí)行某一動(dòng)作Action，Action可被省略。S被稱為該轉(zhuǎn)換的源狀態(tài)，S′被稱為該轉(zhuǎn)換的目標(biāo)狀態(tài)。使用表示一個(gè)轉(zhuǎn)換。當(dāng)g缺省時(shí)，可以省略。當(dāng)轉(zhuǎn)換完成時(shí)，動(dòng)作a將被執(zhí)行。

圖2顯示了一個(gè)該語(yǔ)法的例子：圖2（a）以圖形的形式描述了一個(gè)狀態(tài)圖，圖2（b）顯示了它的樹狀表示。圖2 下方顯示了該狀態(tài)圖在對(duì)應(yīng)的AADL 行為附件代碼?？梢钥闯鰻顟B(tài)A是一個(gè)AND類型的復(fù)合狀態(tài)，并且ENTRY 類型的狀態(tài)和EXIT 類型的狀態(tài)不會(huì)在樹狀圖中出現(xiàn)。

在給出狀態(tài)約束之前，先給出符號(hào)約定。

用謂詞符號(hào)TYPE(s)來(lái)表示。例如：AND(S)為真，表示TYPE(S)=AND。

由于HISTORY也是一種特殊的入口狀態(tài)，因此定義HEntry(S)來(lái)表示一個(gè)狀態(tài)的入口狀態(tài)，當(dāng)HISTORY狀態(tài)存在時(shí)，HEntry(S)=Histroy(S)，否則HEntry(S)為S默認(rèn)入口(ENTRY)狀態(tài)。

定義函數(shù)η-1表示某一狀態(tài)的父狀態(tài)，即：

因此，定義函數(shù)η-2表示某一狀態(tài)的祖父狀態(tài)，即：

Fig.2 Syntax of HBA圖2 HBA語(yǔ)法示例

下面，給出一些約束來(lái)確保HBA的一致性。

（l）只有復(fù)合狀態(tài)才能包括其他狀態(tài)：

（2）AND 類型的復(fù)合狀態(tài)的所有子狀態(tài)都不是basic類型：

（3）XOR 類型的復(fù)合狀態(tài)的子狀態(tài)只有一個(gè)初始狀態(tài)：

（4）語(yǔ)法不支持直接地穿越層次邊界的轉(zhuǎn)換。當(dāng)轉(zhuǎn)換以復(fù)合狀態(tài)作為源狀態(tài)時(shí)，需將復(fù)合狀態(tài)的出口狀態(tài)作為默認(rèn)的源狀態(tài)，例如Exiting transitions。當(dāng)轉(zhuǎn)換以復(fù)合狀態(tài)作為目標(biāo)狀態(tài)時(shí)，需將復(fù)合狀態(tài)的入口狀態(tài)作為默認(rèn)目標(biāo)狀態(tài)，例如“Entering transi-tions”。合法的轉(zhuǎn)換集合在表1中給出。圖3中，黑色實(shí)心點(diǎn)表示入口或出口狀態(tài)，白色空心點(diǎn)表示基本狀態(tài)。規(guī)定轉(zhuǎn)換不能直接從ENTRY類型狀態(tài)到EXIT類型狀態(tài)。

Table 1 Legal transition example表1 合法的轉(zhuǎn)換類型

Fig.3 Legal transitions圖3 合法轉(zhuǎn)換示例圖

4 層次行為附件操作語(yǔ)義

本章定義HBA的形式化操作語(yǔ)義。在HBA中，任一時(shí)刻系統(tǒng)的當(dāng)前狀態(tài)稱之為一個(gè)系統(tǒng)狀態(tài)。每一個(gè)系統(tǒng)狀態(tài)顯示了當(dāng)前系統(tǒng)所包含的信息，即處于激活狀態(tài)的位置的集合、當(dāng)前時(shí)刻變量的賦值和歷史狀態(tài)。

定義2（系統(tǒng)狀態(tài)）系統(tǒng)狀態(tài)的形式為(ρ,μ,θ)，其中：

ρ:S→2S給出了處于激活狀態(tài)的位置。ρ可以理解為η的一個(gè)部分的、動(dòng)態(tài)的版本，它將每一個(gè)復(fù)合狀態(tài)S，映射到S的當(dāng)前被激活的子狀態(tài)。如果一個(gè)復(fù)合狀態(tài)S沒有被激活，那么ρ(S)=?。定義Active(S)=S∈ρ*(root),其中ρ*(S)是S的所有被激活子狀態(tài)的集合，包括S本身。如果S≠root，那么Active(S)?S∈ρ(η-1(S))，其中η-1(S)是S的父狀態(tài)。

μ:Var→? 將實(shí)數(shù)變量映射到它們對(duì)應(yīng)的值。如果?Active(S)，那么對(duì)于ν∈Var(S)，μ(ν)是未定義的，記作μ(v)=⊥。

θ:S→S表示歷史狀態(tài)。將歷史狀態(tài)視作狀態(tài)的一種。如果退出時(shí)復(fù)合狀態(tài)的當(dāng)前子狀態(tài)是一個(gè)基本（BASIC）狀態(tài)時(shí)，θ(S)返回該子狀態(tài)；否則，返回該復(fù)合子狀態(tài)的入口（ENTRY）狀態(tài)。

歷史狀態(tài)：使用謂詞HasHistory(S)=?b∈η(S).History(b)，如果HasHistory(S)存在，那么謂詞HEntry(S)表示S唯一的歷史狀態(tài)。如果謂詞HEntry(S)不存在，那么HEntry(S)表示復(fù)合狀態(tài)S默認(rèn)的入口狀態(tài)。如果S是基本（BASIC）狀態(tài)，那么HEntry(S)=S。如果上述情況都不是，那么HEntry(S)未定義。

定義3（內(nèi)部轉(zhuǎn)換）定義“internal_transition”表示源狀態(tài)和目的狀態(tài)位于同一復(fù)合狀態(tài)內(nèi)的轉(zhuǎn)換。經(jīng)過(guò)該轉(zhuǎn)換，變量的值將會(huì)從V1更新到V2。

為了描述穿越復(fù)合狀態(tài)邊界的轉(zhuǎn)換，定義了“進(jìn)入轉(zhuǎn)換（entering_transition）”和“退出轉(zhuǎn)換（exiting_transition）”。

對(duì)于每個(gè)復(fù)合狀態(tài)，都有一個(gè)默認(rèn)入口狀態(tài)和一個(gè)默認(rèn)出口狀態(tài)。當(dāng)轉(zhuǎn)換以外部狀態(tài)作為源狀態(tài)并以內(nèi)部狀態(tài)作為目標(biāo)狀態(tài)時(shí)，它需要使用進(jìn)入轉(zhuǎn)換。

如圖3 中的Entering 所示，可以看到“進(jìn)入轉(zhuǎn)換”源狀態(tài)的父狀態(tài)（即η-1(S)）和目標(biāo)狀態(tài)的祖父狀態(tài)（即η-2(S1)）是相同的狀態(tài)。進(jìn)入轉(zhuǎn)換分為兩個(gè)步驟：（1）從外部狀態(tài)到復(fù)合狀態(tài)的入口狀態(tài)（即S1）的轉(zhuǎn)換；（2）從入口狀態(tài)到目的狀態(tài)的轉(zhuǎn)換。

當(dāng)轉(zhuǎn)換以內(nèi)部狀態(tài)作為源并將外部狀態(tài)作為目標(biāo)狀態(tài)時(shí)，它需要使用退出轉(zhuǎn)換。

退出轉(zhuǎn)換與進(jìn)入轉(zhuǎn)換類似，但源狀態(tài)的祖父狀態(tài)（即η-2(S1)）和目標(biāo)狀態(tài)的父狀態(tài)（即η-1(S′)）是相同的狀態(tài)。退出轉(zhuǎn)換分為兩個(gè)步驟：（1）從源狀態(tài)到復(fù)合狀態(tài)的出口狀態(tài)（即S1）的轉(zhuǎn)換；（2）從出口狀態(tài)到目的狀態(tài)的轉(zhuǎn)換。

定義4（層次轉(zhuǎn)換）層次轉(zhuǎn)換HT:S→g,aS′是從一個(gè)復(fù)合狀態(tài)遷移到另一個(gè)復(fù)合狀態(tài)的轉(zhuǎn)換。層次轉(zhuǎn)換包括三部分：（1）執(zhí)行“退出轉(zhuǎn)換”，退出復(fù)合狀態(tài)S；（2）執(zhí)行轉(zhuǎn)換本身；（3）執(zhí)行“進(jìn)入轉(zhuǎn)換”，進(jìn)入復(fù)合狀態(tài)S′。

經(jīng)過(guò)層次轉(zhuǎn)換可以得到新的系統(tǒng)狀態(tài)(ρ1,μ1,θ1)，其中：

定義5（狀態(tài)轉(zhuǎn)換）定義狀態(tài)轉(zhuǎn)換Tst：

每個(gè)系統(tǒng)狀態(tài)都由三部分組成：ρ、μ和θ。經(jīng)過(guò)狀態(tài)轉(zhuǎn)換后，系統(tǒng)狀態(tài)將被更新為ρ1、μ1和θ1。

5 圖形化建模工具的實(shí)現(xiàn)

在實(shí)現(xiàn)方面，由于使用Graphiti進(jìn)行圖形化工具開發(fā)需要以EMF（eclipse modeling framework）模型為基礎(chǔ)，因此在圖形化工具開發(fā)之前首先需要對(duì)AADL-HBA 進(jìn)行EMF 模型的建立。由于AADLHBA 是在AADL-BA 基礎(chǔ)上擴(kuò)展，因此本章以擴(kuò)展AADL-BA元模型的方式得到HBA元模型。

5.1 擴(kuò)展AADL行為附件元模型

AADL 行為附件與AADL 核心聯(lián)系緊密，因此AADL行為附件元模型重用了AADL元模型的EMF框架，并在此基礎(chǔ)上加以設(shè)計(jì)。這一方面有利于促進(jìn)AADL-BA 在OSATE2 中的整合；另一方面，使用相同的形式來(lái)制定兩個(gè)元模型可以簡(jiǎn)化對(duì)象依賴關(guān)系的表達(dá)，并簡(jiǎn)化二者之間的模型連接。

圖4 顯示了通過(guò)EMF 擴(kuò)展（例如，Java 的繼承機(jī)制）來(lái)表達(dá)兩個(gè)元模型之間的依賴關(guān)系?？梢钥闯?，BehaviorAnnex擴(kuò)展了AnnexSubclause，BAElement擴(kuò)展了Element。后者簡(jiǎn)化了從AADL-BA模型到AADL模型的鏈接，可以輕松地檢索相應(yīng)的AADL對(duì)象。

為了擴(kuò)展AADL 行為附件，首先擴(kuò)展AADL 元模型，增加并發(fā)狀態(tài)和復(fù)合狀態(tài)的表達(dá)（見圖5 中粗體部分）。

如圖5所示，層次行為附件和AADL行為附件之間的主要區(qū)別在于添加了composite state 和concurrent state。另外，為了符合上述約束，相應(yīng)地添加了諸如進(jìn)入狀態(tài)和退出狀態(tài)的狀態(tài)類型。

Fig.4 AADL-BA meta-model dependency圖4 AADL-BA元模型依賴

Fig.5 Extended AADL behavior annex HBA meta-model(part)圖5 擴(kuò)展后的AADL行為附件HBA元模型（部分）

5.2 使用ANTLR和Xtext技術(shù)生成Java代碼

ANTLR（another tool for language recognition）是一個(gè)解析器生成器，用于讀取、處理、執(zhí)行或翻譯結(jié)構(gòu)化文本或二進(jìn)制文件。它廣泛用于構(gòu)建語(yǔ)言、工具和框架。從語(yǔ)法上看，ANTLR 生成一個(gè)可以構(gòu)建并解析抽象語(yǔ)法樹的解析器。

Xtext 是開發(fā)編程語(yǔ)言和領(lǐng)域特定語(yǔ)言的框架?？梢酝ㄟ^(guò)Xtext 語(yǔ)法來(lái)定義語(yǔ)言，并據(jù)此獲得完整的基礎(chǔ)架構(gòu)，包括解析器、鏈接器、類型檢查器以及編譯器。

使用AADL-HBA builder factory來(lái)指定如何構(gòu)建AADL-HBA 抽象語(yǔ)法樹（abstract syntax tree，AST）。它確保AST 符合AADL-HBA 元模型。使用ANTLR框架從定義的AADL-HBA語(yǔ)法中生成詞法分析器和解析器的Java類。

OSATE 是一個(gè)開源環(huán)境，為基于AADL 的復(fù)雜嵌入式系統(tǒng)開發(fā)架構(gòu)模型提供支持，包括對(duì)AADL的建模和分析。AADL 行為附件插件基于Xtext 技術(shù)，可以在互聯(lián)網(wǎng)上下載AADL 行為附件的元模型（Xtext的輸入）。因此，利用EBNF（extended Backus-Naur form）擴(kuò)展了BA的元模型。

6 HBA到TA的轉(zhuǎn)換

本章介紹層次行為附件（HBA）到時(shí)間自動(dòng)機(jī)（TA）的轉(zhuǎn)換規(guī)則。

雖然David等人提出了層次時(shí)間狀態(tài)機(jī)的概念，并給出了形式化的語(yǔ)法、語(yǔ)義定義，但并沒有進(jìn)一步實(shí)現(xiàn)，也沒有相應(yīng)的集成工具支持。因此，為了使模型能夠被現(xiàn)有工具集分析，給出了一套扁平化算法，用于將HBA 翻譯成現(xiàn)有工具UPPAAL 的輸入——TA，并利用UPPAAL驗(yàn)證模型屬性。

6.1 扁平化算法

在本文的工作中，使用UPPAAL 進(jìn)行形式化驗(yàn)證。正如前面所提到的，需要在驗(yàn)證之前將層次結(jié)構(gòu)扁平化。在UPPAAL 中，每一個(gè)時(shí)間自動(dòng)機(jī)被稱作“模板”，節(jié)點(diǎn)被稱作“位置”。扁平化算法共有8步：

（1）對(duì)于層次行為附件M中的每一個(gè)自動(dòng)機(jī)F，如果F不是頂層自動(dòng)機(jī)，那么該自動(dòng)機(jī)增加一個(gè)新的位置，命名為ReadyState。

（2）對(duì)于每一個(gè)轉(zhuǎn)換t，如果它的目的狀態(tài)是復(fù)合狀態(tài)S（composite或concurrent狀態(tài)），那么增加一個(gè)從ReadyState狀態(tài)到S的入口狀態(tài)的轉(zhuǎn)換，并且轉(zhuǎn)換的警衛(wèi)條件與轉(zhuǎn)換t的警衛(wèi)條件一致。

（3）為了同步多個(gè)相關(guān)自動(dòng)機(jī)的執(zhí)行，對(duì)于所有目的狀態(tài)是復(fù)合狀態(tài)的轉(zhuǎn)換t，為其增加一個(gè)發(fā)送同步信號(hào)，記為發(fā)送（?。?/p>

（4）對(duì)于每個(gè)XOR類型的復(fù)合狀態(tài)S（composite狀態(tài)），為其對(duì)應(yīng)的子狀態(tài)機(jī)，增加的從ReadyState狀態(tài)到S的入口狀態(tài)的轉(zhuǎn)換，為該轉(zhuǎn)換增加接收同步信號(hào)，記作接收（？），同步信號(hào)與（3）中相同。

（5）對(duì)于AND 類型的復(fù)合狀態(tài)S（concurrent 狀態(tài)），為其每個(gè)子狀態(tài)機(jī)，增加的從ReadyState狀態(tài)到S的入口狀態(tài)的轉(zhuǎn)換，為該轉(zhuǎn)換增加接收同步信號(hào)，記作接收（？），同步信號(hào)與（3）中相同。

（6）同理，對(duì)于所有源狀態(tài)是復(fù)合狀態(tài)的轉(zhuǎn)換t，為其增加一個(gè)接收同步信號(hào)，記為接收（?）。

（7）對(duì)于每個(gè)XOR類型的復(fù)合狀態(tài)S（composite狀態(tài)），為其對(duì)應(yīng)的子狀態(tài)機(jī)，增加的從S的出口狀態(tài)到ReadyState狀態(tài)的轉(zhuǎn)換，并為該轉(zhuǎn)換增加發(fā)送同步信號(hào)，記作接收（?。叫盘?hào)與（6）中相同。

（8）對(duì)于AND 類型的復(fù)合狀態(tài)S（concurrent 狀態(tài)），為其每個(gè)子狀態(tài)機(jī)，增加的從出口狀態(tài)到ReadyState 狀態(tài)的轉(zhuǎn)換，為該轉(zhuǎn)換增加發(fā)送同步信號(hào)，記作發(fā)送（！），同步信號(hào)與（6）中相同。

6.2 轉(zhuǎn)換規(guī)則

首先簡(jiǎn)單介紹時(shí)間自動(dòng)機(jī)TA 的語(yǔ)法定義。一個(gè)時(shí)間自動(dòng)機(jī)A是一個(gè)六元組。其中，L是一個(gè)有窮的位置集合；L0?L是初始位置的集合；Σ是一個(gè)有窮符號(hào)集合；X是一個(gè)有窮時(shí)鐘的集合；I是一個(gè)映射，它給L中的每個(gè)位置s指定Φ(x)中的一個(gè)時(shí)鐘約束；E?L×Σ×2X×Φ(X)×L是一個(gè)轉(zhuǎn)換集合。表示輸入符號(hào)a時(shí)，從位置s到s′的轉(zhuǎn)換。φ是X上的一個(gè)時(shí)鐘約束，它在轉(zhuǎn)變發(fā)生時(shí)被滿足；λ?X是在該轉(zhuǎn)換發(fā)生時(shí)復(fù)位零值的時(shí)鐘集合。

由于扁平化后的HBA 與TA 有著相同的自動(dòng)機(jī)形式，因此可以通過(guò)簡(jiǎn)單的映射規(guī)則完成HBA到TA的映射。

7 案例分析

在實(shí)際工程中，對(duì)導(dǎo)航、制導(dǎo)與控制系統(tǒng)（guidance,navigation and control system），即GNC系統(tǒng)建模并生成初始模型。由于文章空間的限制，只在本文中介紹GNC 系統(tǒng)中的姿態(tài)控制線程的精化，作為本文的演示。

7.1 姿態(tài)控制線程

7.1.1 需求描述

姿態(tài)控制線程有4 個(gè)狀態(tài)：姿態(tài)控制狀態(tài)、穩(wěn)定狀態(tài)、遙測(cè)狀態(tài)、系統(tǒng)監(jiān)測(cè)狀態(tài)。姿態(tài)控制線程的功能行為如圖6所示。假設(shè)此時(shí)衛(wèi)星已正常運(yùn)行，處于穩(wěn)定狀態(tài)（實(shí)際案例中當(dāng)星箭分離后，衛(wèi)星需要先通過(guò)姿態(tài)控制和軌道控制調(diào)整自身位置后，再進(jìn)入穩(wěn)定狀態(tài)）。其中穩(wěn)定狀態(tài)為初始狀態(tài)。當(dāng)衛(wèi)星處于穩(wěn)定狀態(tài)時(shí)，若接收到姿態(tài)調(diào)整指令，則進(jìn)入姿態(tài)控制狀態(tài)；若接收到遙測(cè)指令，則進(jìn)入遙測(cè)狀態(tài)；若接收到系統(tǒng)監(jiān)測(cè)指令，則進(jìn)入系統(tǒng)監(jiān)測(cè)狀態(tài)。當(dāng)姿態(tài)調(diào)整完成后，衛(wèi)星將發(fā)送姿態(tài)調(diào)整完成信號(hào)，并返回穩(wěn)定狀態(tài)。當(dāng)遙測(cè)狀態(tài)結(jié)束時(shí)，衛(wèi)星將發(fā)送遙測(cè)結(jié)束信號(hào)，并返回穩(wěn)定狀態(tài)。當(dāng)衛(wèi)星處于系統(tǒng)監(jiān)測(cè)狀態(tài)時(shí)，若接收到監(jiān)測(cè)終止指令，衛(wèi)星將返回穩(wěn)定狀態(tài)。

Fig.6 Attitude control thread functional behavior圖6 姿態(tài)控制線程的功能行為

上述需求是架構(gòu)設(shè)計(jì)師設(shè)計(jì)的，他們可能不會(huì)考慮每個(gè)模塊的內(nèi)部處理細(xì)節(jié)。內(nèi)部細(xì)節(jié)將在精化階段由設(shè)計(jì)人員補(bǔ)充。

7.1.2 使用行為附件建模

此處，行為附件用來(lái)建模第一次的精化行為。AADL代碼如下所示：

上述案例對(duì)應(yīng)的圖形化效果如圖7所示。

7.2 精化

7.2.1 需求精化

以姿態(tài)控制模塊為例，介紹各模塊的精化。姿態(tài)控制包括滾動(dòng)姿態(tài)機(jī)動(dòng)狀態(tài)、姿態(tài)偏置飛行狀態(tài)、滾動(dòng)姿態(tài)返回狀態(tài)三個(gè)正常狀態(tài)以及陀螺儀安全、飛輪安全狀態(tài)兩個(gè)異常狀態(tài)。姿態(tài)控制模塊的功能行為如圖8所示。

當(dāng)接收到姿態(tài)調(diào)整指令后，系統(tǒng)進(jìn)入姿態(tài)機(jī)動(dòng)狀態(tài)。檢查三軸（X、Y、Z軸）飛輪角動(dòng)量值與陀螺儀狀態(tài)，若三軸同時(shí)滿足角動(dòng)量不大于4 Nms，并且陀螺儀可用，則進(jìn)入姿態(tài)偏置飛行狀態(tài)；否則，若角動(dòng)量不滿足上述條件，則進(jìn)入角動(dòng)量調(diào)整狀態(tài)；若陀螺儀不可用，則進(jìn)入陀螺儀安全狀態(tài)。

Fig.8 Control state functional behavior圖8 控制狀態(tài)內(nèi)部的功能行為

當(dāng)衛(wèi)星處于偏置飛行狀態(tài)時(shí)，若控制姿態(tài)角大于或等于13°，則進(jìn)入飛輪安全狀態(tài)；否則，偏置飛行結(jié)束后，進(jìn)入姿態(tài)返回狀態(tài)。

姿態(tài)返回狀態(tài)發(fā)送姿態(tài)調(diào)整信號(hào)后，退出姿態(tài)控制狀態(tài)。

7.2.2 使用層次行為附件建模

使用層次行為附件對(duì)姿態(tài)控制模塊建模。首先將姿態(tài)控制狀態(tài)設(shè)置為復(fù)合狀態(tài)（composite state），然后為姿態(tài)控制狀態(tài)添加子狀態(tài)描述，HBA 代碼如下所示：

當(dāng)雙擊圖7中的ControlState后，可以看到圖9所示的自動(dòng)機(jī)。

7.3 形式化驗(yàn)證

根據(jù)第6 章提出的轉(zhuǎn)換規(guī)則，將上述HBA 轉(zhuǎn)換為UPPAAL 的輸入——時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)，如圖10 所示。本章中詳細(xì)描述的頂層模塊和姿態(tài)控制模塊對(duì)應(yīng)的時(shí)間自動(dòng)機(jī)如圖11和圖12所示。

在此基礎(chǔ)上，可以對(duì)死鎖、安全性、活性等性質(zhì)進(jìn)行驗(yàn)證，例如：

（1）系統(tǒng)不存在死鎖，A[]!deadlock。

（2）安全性，如“當(dāng)系統(tǒng)處于姿態(tài)控制狀態(tài)時(shí)，機(jī)動(dòng)狀態(tài)一定會(huì)被激活”，A[](ac.ControlState)imply(atcm.Maneuver)。

（3）活性，如“系統(tǒng)終究會(huì)進(jìn)入穩(wěn)定模式”，E＜＞(ac.StableState)。

通過(guò)將上述待驗(yàn)證性質(zhì)輸入到UPPAAL 的驗(yàn)證器中后，得到如圖13 所示結(jié)果。從結(jié)果圖中可以看出，系統(tǒng)不滿足“系統(tǒng)無(wú)死鎖”性質(zhì)。

Fig.9 Control state graphical display圖9 控制狀態(tài)內(nèi)部的圖形化展示

Fig.10 TA network of attitude control thread圖10 姿態(tài)控制線程的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)

Fig.11 TA representation of attitude control thread圖11 姿態(tài)控制線程的時(shí)間自動(dòng)機(jī)表示

Fig.12 TA representation of attitude control state圖12 姿態(tài)控制狀態(tài)內(nèi)部的時(shí)間自動(dòng)機(jī)表示

Fig.13 Verification result of attitude control thread圖13 姿態(tài)控制線程驗(yàn)證結(jié)果

經(jīng)分析查驗(yàn)發(fā)現(xiàn)，在需求描述中，針對(duì)頂層姿態(tài)控制線程有如下時(shí)間屬性描述：姿態(tài)控制線程周期性調(diào)度，調(diào)度周期為360 ms。在穩(wěn)定模塊中，有如下屬性描述：在穩(wěn)定模塊中，當(dāng)系統(tǒng)處于數(shù)據(jù)采集（dataCol）階段，若在一個(gè)線程周期內(nèi)未收到數(shù)據(jù)信息，則使用上一周期數(shù)據(jù)進(jìn)行檢測(cè)；若連續(xù)三次未收到數(shù)據(jù)信息，則報(bào)告數(shù)據(jù)采集異常。當(dāng)收到數(shù)據(jù)信息后，經(jīng)過(guò)600 ms 延遲，確認(rèn)無(wú)新數(shù)據(jù)到達(dá)時(shí)，進(jìn)入數(shù)據(jù)校驗(yàn)（check）階段。

通過(guò)查看反例和仿真，發(fā)現(xiàn)系統(tǒng)上述需求會(huì)導(dǎo)致系統(tǒng)停留在穩(wěn)定模塊中的數(shù)據(jù)采集階段，當(dāng)一個(gè)線程周期（60 ms）結(jié)束后，未達(dá)到600 ms 延遲的要求，因此系統(tǒng)無(wú)法繼續(xù)遷移。針對(duì)上述問(wèn)題，將系統(tǒng)延遲時(shí)間縮小后更新模型，發(fā)現(xiàn)系統(tǒng)無(wú)死鎖。

8 相關(guān)工作

在層次擴(kuò)展方面，Harel[15]通過(guò)擴(kuò)展UML 狀態(tài)機(jī)圖提出了層次自動(dòng)機(jī)的概念，解決了復(fù)雜系統(tǒng)狀態(tài)機(jī)規(guī)模大、層次嵌套深的問(wèn)題，但嵌入式安全關(guān)鍵軟件的實(shí)時(shí)性描述仍然缺乏。為了解決時(shí)間自動(dòng)機(jī)無(wú)法描述層次模型的問(wèn)題，David[11]提出了層次時(shí)間自動(dòng)機(jī)（HTA）的概念，并通過(guò)擴(kuò)展時(shí)間自動(dòng)機(jī)來(lái)解決復(fù)雜的層次系統(tǒng)建模和驗(yàn)證問(wèn)題。HTA可以建模分層系統(tǒng)并驗(yàn)證它們的時(shí)間屬性，但它需要將模型手動(dòng)轉(zhuǎn)換為自動(dòng)機(jī)形式，這增加了工作的復(fù)雜性。

在形式化語(yǔ)法和語(yǔ)義方面，David[11]給出了層次化擴(kuò)展的HTA 的形式化語(yǔ)法和操作語(yǔ)義，并給出了一個(gè)簡(jiǎn)化的HTA模型。Yang等人[8]通過(guò)時(shí)間抽象狀態(tài)機(jī)（time abstract state machine，TASM）定義了AADL行為附件的形式語(yǔ)義，并提出了一個(gè)實(shí)時(shí)行為建模和驗(yàn)證原型。Zhou等人[16]給出了UML狀態(tài)機(jī)圖的基本語(yǔ)義和MARTE（modeling and analysis of real time and embedded systems）的時(shí)間依賴建模元素，并提出了基于擴(kuò)展層次結(jié)構(gòu)的操作語(yǔ)義的形式化時(shí)間自動(dòng)機(jī)。?lveczky 等人[17]為AADL 的行為子集提供了一個(gè)形式化的實(shí)時(shí)重寫邏輯語(yǔ)義，其中包括其行為附件的基本方面。為了在AADL架構(gòu)下支持明確的推理、形式化驗(yàn)證以及高保真仿真，Besnard等人[18]定義了AADL 行為附件的形式語(yǔ)義。Larson 等人[19]提出了嵌入式系統(tǒng)軟件的行為語(yǔ)言（behavioral language of embedded system software，BLESS），它是AADL 的行為接口規(guī)范語(yǔ)言和證明環(huán)境。BLESS為AADL行為描述和自動(dòng)生成驗(yàn)證條件提供了形式語(yǔ)義。Ahmad等人[20]提出了AADL模型的同步子集的形式語(yǔ)義。通過(guò)使用他們開發(fā)的定理證明器——HHL（hybrid hoare logic）prover 可以驗(yàn)證AADL 模型的正確性。Johnsen等人[21]對(duì)AADL核心的一個(gè)子集進(jìn)行了形式化，并將其轉(zhuǎn)換為UPPAAL 的輸入語(yǔ)言TA。他們通過(guò)語(yǔ)義錨定的方法將AADL 子集映射到時(shí)間自動(dòng)機(jī)，給出了AADL子集的形式化語(yǔ)義定義。Fran?a等人[12]分別通過(guò)實(shí)際工程項(xiàng)目評(píng)估了AADL-BA 的實(shí)用性，分析了AADL-BA 的約束條件，提出了行為附件層次化擴(kuò)展的思想，但沒有給出形式化定義和實(shí)現(xiàn)。

在混合建模方面，Ma 等人[22]使用高級(jí)建模語(yǔ)言AADL 進(jìn)行系統(tǒng)架構(gòu)設(shè)計(jì)；使用基于同步語(yǔ)言SIGNAL的形式化框架Polychrony進(jìn)行分析和驗(yàn)證。Yu等人[23]通過(guò)利用AADL 對(duì)嵌入式系統(tǒng)架構(gòu)建模和利用Simulink對(duì)嵌入式系統(tǒng)功能建模，并通過(guò)形式化的多時(shí)鐘模型分析和驗(yàn)證了系統(tǒng)的時(shí)間屬性。

9 總結(jié)與展望

本文通過(guò)擴(kuò)展AADL 行為附件元模型的方式，對(duì)AADL功能行為描述能力進(jìn)行了層次化擴(kuò)展。通過(guò)提出層次行為附件（HBA）的方法，解決了建模過(guò)程中難以管理大量狀態(tài)以及結(jié)構(gòu)層次丟失的問(wèn)題。本文給出了層次行為附件的形式化語(yǔ)法約束以及形式化語(yǔ)義定義，通過(guò)對(duì)AADL 行為附件元模型的擴(kuò)展，基于Xtext以及Xtend技術(shù)，在AADL開源開發(fā)環(huán)境OSATE上實(shí)現(xiàn)了對(duì)應(yīng)的工具插件。為了便于形式化驗(yàn)證，本文給出了HBA到時(shí)間自動(dòng)機(jī)TA的轉(zhuǎn)換規(guī)則。最后，通過(guò)案例分析，驗(yàn)證了方法的有效性。

AADL行為附件自身支持timeout、dispatch、computation 等時(shí)間相關(guān)描述，本文所提層次行為附件擴(kuò)展主要關(guān)注組件功能行為的描述，對(duì)原有時(shí)間屬性沒有擴(kuò)展。因此，擴(kuò)展后的層次行為附件仍然支持原AADL行為附件支持的時(shí)間描述。對(duì)于層次化擴(kuò)展而引入的時(shí)間相關(guān)屬性的計(jì)算與判別問(wèn)題，是下一步研究工作的重點(diǎn)。