系統架構描述語言AADL的功能行為建模擴展*

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

1.南京航空航天大學 計算機科學與技術學院，南京210016

2.高安全系統的軟件開發與驗證技術工信部重點實驗室，南京210016

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

1 引言

嵌入式系統廣泛應用于航空、航天、核能等領域，這些系統具有資源受限、交互頻繁等特點，對實時性、可靠性等性質有非常高的要求，因此也稱為安全關鍵系統（safety-critical systems）。由于功能和非功能要求不斷提高，系統的復雜度急劇增加。如何設計與實現高質量的安全關鍵嵌入式系統，并有效控制開發時間和成本，是學術界和工業界共同面臨的難題。近年來，模型驅動開發方法（model-driven development，MDD）逐漸成為安全關鍵系統設計與開發的重要手段[1]。

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

嵌入式系統的功能行為建模包括控制流建模與數據流建模。如圖1所示，給出了AADL功能行為建模擴展的總體框架，包括基于行為附件對控制流功能行為建模以及基于同步語言SIGNAL[6]對數據流功能行為建模。

Fig.1 Global view of AADL functional modeling圖1 AADL功能行為建模總體框架

為了支持組件內部的控制流建模，法國IRIT實驗室于2006年提出了AADL行為附件（behavior annex）[7]。行為附件以變遷系統（transition system）的形式增強了AADL線程構件和子程序構件功能行為的詳細描述能力[8]。行為附件與執行模型有密切的關系：執行模型定義行為附件何時執行，哪些數據被改變，而行為附件處于構件內部，對線程、子程序構件的執行給予更精確的描述[9]。

在對工業實際案例建模過程中，可能存在如下問題：（1）建模實際的工業項目是一個不斷精化的過程，扁平化的狀態機難以適應頻繁的精化。（2）工業界的實際項目中有許多復雜的多層嵌套的層次狀態機。如果這些嵌套狀態機被展開，將會形成一個巨大且難以管理的狀態機圖。（3）扁平化模型難以管理大量的組件，并且扁平化模型會造成結構信息的丟失。因此，對于AADL行為附件來說，層次化地表達功能行為是一個非常重要的特征。

為了解決扁平狀態機的問題，Elattar等人擴展了UML 狀態圖Statecharts[10]。相應地，David 提出了層次時間狀態機（hierarchical timed automata，HTA）[11]的概念，用于解決UPPAAL 中的層次化建模問題。另外，Fran?a 等人[12]通過對飛行控制軟件的實際建模，評估了AADL 行為附件，提出了在AADL 行為附件中引入層次化概念的想法。然而，他們沒有給出形式化的語法、語義定義以及層次化擴展的實現。

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

本文的其余部分結構如下：第2章介紹了AADL和行為附件；第3 章給出了HBA 的語法定義；第4 章定義了HBA 的形式語義；第5 章介紹了AADL 行為附件層次化擴展的實現；第6 章給出了HBA 到TA（timed automata）的轉換規則；第7章介紹了一個實際的工業案例研究；第8 章討論相關工作；第9 章給出結論。

2 研究背景

2.1 AADL語言簡介

AADL 是一種專為嵌入式系統建模而設計的架構描述語言。它支持高度可演化系統的開發，系統架構的早期分析，以及用于整個生命周期持續分析的架構模型的演變。

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

（1）線程、線程組、子程序、數據、進程。

（2）處理器、內存、總線、外設。

（3）用系統表示軟件和執行平臺的組合集。

例如，一個線程表示一個連續的執行流程，它是唯一可以被調度的AADL組件。一個子程序表示一段可以被線程或另一個子程序調用的代碼。

組件之間的通信可以通過數據流、子程序調用或訪問共享變量來實現。這些不同的通信方式在通信組件的接口中聲明。根據所選擇的通信方式實例，通信連接點可能是端口（port）、子程序（subprogram）或數據訪問（data access）[8]。

系統行為不僅依賴于上述組件及其連接所定義的體系結構，還依賴于運行時環境[13]。AADL標準將執行模型指定為虛擬運行時環境（包含同步和異步模式），以支持組件的執行和管理。在執行模型中也定義了諸如截止日期、調度時間等時間屬性，這些屬性通過AADL屬性聲明。

此外，AADL 支持兩種擴展方式：屬性集和附件。屬性集擴展允許用戶引入新的屬性集。例如，調度分析工具Cheddar，通過定義新的屬性集增強了AADL支持更復雜調度算法的能力。現有的附件包括AADL錯誤模型附件[14]、AADL行為附件[7]、ARINC653附件、數據模型附件等。

2.2 AADL行為附件

行為附件是執行模型調度機制的擴展，用于更精確地描述模型行為，例如端口通信、子程序調用、時序、異步等。AADL執行模型指定行為附件何時執行，并指定哪些數據被執行。完整的AADL 模型應該包括執行模型和行為附件。現在行為附件可以附加到AADL 的任何組件中。它通過擴展的AADL 模式自動機[7]來描述組件行為，例如：“initial”指定自動機的初始狀態，“complete”指定線程完成，轉換可以包括條件和動作，條件和動作包括發送或接收事件，調用或執行子程序等。

行為附件主要包括三部分：變量、狀態和轉換。變量部分聲明當前行為附件中使用的所有局部變量。局部變量可以用來保存當前行為附件范圍內的中間結果。狀態部分枚舉狀態機的所有狀態及其屬性（initial，complete，final 或它們的組合）。默認狀態是一個執行狀態。轉換定義了從源狀態到目標狀態的轉換，轉換可以有條件和動作。

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

3 層次行為附件（HBA）語法

HBA擴展了AADL行為附件以增強行為附件的層次描述能力。HBA 保留AADL 行為附件的變量、狀態和轉換，添加層次映射函數和復合狀態。

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

Var是自動機中使用的局部變量的有限集合。S是一個非空有限的狀態集合。S0?S是初始狀態的有限集合。η:S→2S是層次函數，它將S映射到S的所有可達的子狀態上。映射η將會產生一個根節點為root的樹結構，其中root∈S。通過η來記錄某狀態S與其子狀態的層次關系。type窮舉了所有狀態的類型。復合狀態是AND 或者XOR 類型。非復合狀態是基本狀態（BASIC）、入口狀態（ENTRY）、出口狀態（EXIT）或歷史狀態（HISTORY）中的一種。

AND狀態表示該復合狀態的所有子狀態是并發執行的，即當父狀態被執行時，其內部各子狀態同時從各自的初始狀態開始執行。在后續的HBA 實現中，將AND 狀態表示為“concurrent state”。XOR 表示該復合狀態內的所有子狀態是互斥執行，即同一時刻有且僅有一個子狀態被執行。在后續的HBA實現中，將AND狀態表示為“composite state”。ENTRY狀態表示該非復合狀態是其父狀態的入口狀態，即當進入其父狀態時，默認進入該子狀態。EXIT 狀態表示該非復合狀態為出口狀態，即將要從其父狀態轉移到下一狀態時，由該狀態轉移至下一狀態。HISTORY 狀態是一個偽狀態，其目的是記住從組合狀態中退出時所處的子狀態，當再次進入組合狀態時，可直接進入這個子狀態，而不是再次從組合狀態的ENTRY狀態開始。

T?s×(Guard×Action)×s是轉換函數。一個轉換連接兩個狀態S和S′，轉換有一個條件guard，或為布爾值。轉換完成時可執行某一動作Action，Action可被省略。S被稱為該轉換的源狀態，S′被稱為該轉換的目標狀態。使用表示一個轉換。當g缺省時，可以省略。當轉換完成時，動作a將被執行。

圖2顯示了一個該語法的例子：圖2（a）以圖形的形式描述了一個狀態圖，圖2（b）顯示了它的樹狀表示。圖2 下方顯示了該狀態圖在對應的AADL 行為附件代碼。可以看出狀態A是一個AND類型的復合狀態，并且ENTRY 類型的狀態和EXIT 類型的狀態不會在樹狀圖中出現。

在給出狀態約束之前，先給出符號約定。

用謂詞符號TYPE(s)來表示。例如：AND(S)為真，表示TYPE(S)=AND。

由于HISTORY也是一種特殊的入口狀態，因此定義HEntry(S)來表示一個狀態的入口狀態，當HISTORY狀態存在時，HEntry(S)=Histroy(S)，否則HEntry(S)為S默認入口(ENTRY)狀態。

定義函數η-1表示某一狀態的父狀態，即：

因此，定義函數η-2表示某一狀態的祖父狀態，即：

Fig.2 Syntax of HBA圖2 HBA語法示例

下面，給出一些約束來確保HBA的一致性。

（l）只有復合狀態才能包括其他狀態：

（2）AND 類型的復合狀態的所有子狀態都不是basic類型：

（3）XOR 類型的復合狀態的子狀態只有一個初始狀態：

（4）語法不支持直接地穿越層次邊界的轉換。當轉換以復合狀態作為源狀態時，需將復合狀態的出口狀態作為默認的源狀態，例如Exiting transitions。當轉換以復合狀態作為目標狀態時，需將復合狀態的入口狀態作為默認目標狀態，例如“Entering transi-tions”。合法的轉換集合在表1中給出。圖3中，黑色實心點表示入口或出口狀態，白色空心點表示基本狀態。規定轉換不能直接從ENTRY類型狀態到EXIT類型狀態。

Table 1 Legal transition example表1 合法的轉換類型

Fig.3 Legal transitions圖3 合法轉換示例圖

4 層次行為附件操作語義

本章定義HBA的形式化操作語義。在HBA中，任一時刻系統的當前狀態稱之為一個系統狀態。每一個系統狀態顯示了當前系統所包含的信息，即處于激活狀態的位置的集合、當前時刻變量的賦值和歷史狀態。

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

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

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

θ:S→S表示歷史狀態。將歷史狀態視作狀態的一種。如果退出時復合狀態的當前子狀態是一個基本（BASIC）狀態時，θ(S)返回該子狀態；否則，返回該復合子狀態的入口（ENTRY）狀態。

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

定義3（內部轉換）定義“internal_transition”表示源狀態和目的狀態位于同一復合狀態內的轉換。經過該轉換，變量的值將會從V1更新到V2。

為了描述穿越復合狀態邊界的轉換，定義了“進入轉換（entering_transition）”和“退出轉換（exiting_transition）”。

對于每個復合狀態，都有一個默認入口狀態和一個默認出口狀態。當轉換以外部狀態作為源狀態并以內部狀態作為目標狀態時，它需要使用進入轉換。

如圖3 中的Entering 所示，可以看到“進入轉換”源狀態的父狀態（即η-1(S)）和目標狀態的祖父狀態（即η-2(S1)）是相同的狀態。進入轉換分為兩個步驟：（1）從外部狀態到復合狀態的入口狀態（即S1）的轉換；（2）從入口狀態到目的狀態的轉換。

當轉換以內部狀態作為源并將外部狀態作為目標狀態時，它需要使用退出轉換。

退出轉換與進入轉換類似，但源狀態的祖父狀態（即η-2(S1)）和目標狀態的父狀態（即η-1(S′)）是相同的狀態。退出轉換分為兩個步驟：（1）從源狀態到復合狀態的出口狀態（即S1）的轉換；（2）從出口狀態到目的狀態的轉換。

定義4（層次轉換）層次轉換HT:S→g,aS′是從一個復合狀態遷移到另一個復合狀態的轉換。層次轉換包括三部分：（1）執行“退出轉換”，退出復合狀態S；（2）執行轉換本身；（3）執行“進入轉換”，進入復合狀態S′。

經過層次轉換可以得到新的系統狀態(ρ1,μ1,θ1)，其中：

定義5（狀態轉換）定義狀態轉換Tst：

每個系統狀態都由三部分組成：ρ、μ和θ。經過狀態轉換后，系統狀態將被更新為ρ1、μ1和θ1。

5 圖形化建模工具的實現

在實現方面，由于使用Graphiti進行圖形化工具開發需要以EMF（eclipse modeling framework）模型為基礎，因此在圖形化工具開發之前首先需要對AADL-HBA 進行EMF 模型的建立。由于AADLHBA 是在AADL-BA 基礎上擴展，因此本章以擴展AADL-BA元模型的方式得到HBA元模型。

5.1 擴展AADL行為附件元模型

AADL 行為附件與AADL 核心聯系緊密，因此AADL行為附件元模型重用了AADL元模型的EMF框架，并在此基礎上加以設計。這一方面有利于促進AADL-BA 在OSATE2 中的整合；另一方面，使用相同的形式來制定兩個元模型可以簡化對象依賴關系的表達，并簡化二者之間的模型連接。

圖4 顯示了通過EMF 擴展（例如，Java 的繼承機制）來表達兩個元模型之間的依賴關系。可以看出，BehaviorAnnex擴展了AnnexSubclause，BAElement擴展了Element。后者簡化了從AADL-BA模型到AADL模型的鏈接，可以輕松地檢索相應的AADL對象。

為了擴展AADL 行為附件，首先擴展AADL 元模型，增加并發狀態和復合狀態的表達（見圖5 中粗體部分）。

如圖5所示，層次行為附件和AADL行為附件之間的主要區別在于添加了composite state 和concurrent state。另外，為了符合上述約束，相應地添加了諸如進入狀態和退出狀態的狀態類型。

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

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

5.2 使用ANTLR和Xtext技術生成Java代碼

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

Xtext 是開發編程語言和領域特定語言的框架。可以通過Xtext 語法來定義語言，并據此獲得完整的基礎架構，包括解析器、鏈接器、類型檢查器以及編譯器。

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

OSATE 是一個開源環境，為基于AADL 的復雜嵌入式系統開發架構模型提供支持，包括對AADL的建模和分析。AADL 行為附件插件基于Xtext 技術，可以在互聯網上下載AADL 行為附件的元模型（Xtext的輸入）。因此，利用EBNF（extended Backus-Naur form）擴展了BA的元模型。

6 HBA到TA的轉換

本章介紹層次行為附件（HBA）到時間自動機（TA）的轉換規則。

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

6.1 扁平化算法

在本文的工作中，使用UPPAAL 進行形式化驗證。正如前面所提到的，需要在驗證之前將層次結構扁平化。在UPPAAL 中，每一個時間自動機被稱作“模板”，節點被稱作“位置”。扁平化算法共有8步：

（1）對于層次行為附件M中的每一個自動機F，如果F不是頂層自動機，那么該自動機增加一個新的位置，命名為ReadyState。

（2）對于每一個轉換t，如果它的目的狀態是復合狀態S（composite或concurrent狀態），那么增加一個從ReadyState狀態到S的入口狀態的轉換，并且轉換的警衛條件與轉換t的警衛條件一致。

（3）為了同步多個相關自動機的執行，對于所有目的狀態是復合狀態的轉換t，為其增加一個發送同步信號，記為發送（！）。

（4）對于每個XOR類型的復合狀態S（composite狀態），為其對應的子狀態機，增加的從ReadyState狀態到S的入口狀態的轉換，為該轉換增加接收同步信號，記作接收（？），同步信號與（3）中相同。

（5）對于AND 類型的復合狀態S（concurrent 狀態），為其每個子狀態機，增加的從ReadyState狀態到S的入口狀態的轉換，為該轉換增加接收同步信號，記作接收（？），同步信號與（3）中相同。

（6）同理，對于所有源狀態是復合狀態的轉換t，為其增加一個接收同步信號，記為接收（?）。

（7）對于每個XOR類型的復合狀態S（composite狀態），為其對應的子狀態機，增加的從S的出口狀態到ReadyState狀態的轉換，并為該轉換增加發送同步信號，記作接收（！），同步信號與（6）中相同。

（8）對于AND 類型的復合狀態S（concurrent 狀態），為其每個子狀態機，增加的從出口狀態到ReadyState 狀態的轉換，為該轉換增加發送同步信號，記作發送（！），同步信號與（6）中相同。

6.2 轉換規則

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

由于扁平化后的HBA 與TA 有著相同的自動機形式，因此可以通過簡單的映射規則完成HBA到TA的映射。

7 案例分析

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

7.1 姿態控制線程

7.1.1 需求描述

姿態控制線程有4 個狀態：姿態控制狀態、穩定狀態、遙測狀態、系統監測狀態。姿態控制線程的功能行為如圖6所示。假設此時衛星已正常運行，處于穩定狀態（實際案例中當星箭分離后，衛星需要先通過姿態控制和軌道控制調整自身位置后，再進入穩定狀態）。其中穩定狀態為初始狀態。當衛星處于穩定狀態時，若接收到姿態調整指令，則進入姿態控制狀態；若接收到遙測指令，則進入遙測狀態；若接收到系統監測指令，則進入系統監測狀態。當姿態調整完成后，衛星將發送姿態調整完成信號，并返回穩定狀態。當遙測狀態結束時，衛星將發送遙測結束信號，并返回穩定狀態。當衛星處于系統監測狀態時，若接收到監測終止指令，衛星將返回穩定狀態。

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

上述需求是架構設計師設計的，他們可能不會考慮每個模塊的內部處理細節。內部細節將在精化階段由設計人員補充。

7.1.2 使用行為附件建模

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

上述案例對應的圖形化效果如圖7所示。

7.2 精化

7.2.1 需求精化

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

當接收到姿態調整指令后，系統進入姿態機動狀態。檢查三軸（X、Y、Z軸）飛輪角動量值與陀螺儀狀態，若三軸同時滿足角動量不大于4 Nms，并且陀螺儀可用，則進入姿態偏置飛行狀態；否則，若角動量不滿足上述條件，則進入角動量調整狀態；若陀螺儀不可用，則進入陀螺儀安全狀態。

Fig.8 Control state functional behavior圖8 控制狀態內部的功能行為

當衛星處于偏置飛行狀態時，若控制姿態角大于或等于13°，則進入飛輪安全狀態；否則，偏置飛行結束后，進入姿態返回狀態。

姿態返回狀態發送姿態調整信號后，退出姿態控制狀態。

7.2.2 使用層次行為附件建模

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

當雙擊圖7中的ControlState后，可以看到圖9所示的自動機。

7.3 形式化驗證

根據第6 章提出的轉換規則，將上述HBA 轉換為UPPAAL 的輸入——時間自動機網絡，如圖10 所示。本章中詳細描述的頂層模塊和姿態控制模塊對應的時間自動機如圖11和圖12所示。

在此基礎上，可以對死鎖、安全性、活性等性質進行驗證，例如：

（1）系統不存在死鎖，A[]!deadlock。

（2）安全性，如“當系統處于姿態控制狀態時，機動狀態一定會被激活”，A[](ac.ControlState)imply(atcm.Maneuver)。

（3）活性，如“系統終究會進入穩定模式”，E＜＞(ac.StableState)。

通過將上述待驗證性質輸入到UPPAAL 的驗證器中后，得到如圖13 所示結果。從結果圖中可以看出，系統不滿足“系統無死鎖”性質。

Fig.9 Control state graphical display圖9 控制狀態內部的圖形化展示

Fig.10 TA network of attitude control thread圖10 姿態控制線程的時間自動機網絡

Fig.11 TA representation of attitude control thread圖11 姿態控制線程的時間自動機表示

Fig.12 TA representation of attitude control state圖12 姿態控制狀態內部的時間自動機表示

Fig.13 Verification result of attitude control thread圖13 姿態控制線程驗證結果

經分析查驗發現，在需求描述中，針對頂層姿態控制線程有如下時間屬性描述：姿態控制線程周期性調度，調度周期為360 ms。在穩定模塊中，有如下屬性描述：在穩定模塊中，當系統處于數據采集（dataCol）階段，若在一個線程周期內未收到數據信息，則使用上一周期數據進行檢測；若連續三次未收到數據信息，則報告數據采集異常。當收到數據信息后，經過600 ms 延遲，確認無新數據到達時，進入數據校驗（check）階段。

通過查看反例和仿真，發現系統上述需求會導致系統停留在穩定模塊中的數據采集階段，當一個線程周期（60 ms）結束后，未達到600 ms 延遲的要求，因此系統無法繼續遷移。針對上述問題，將系統延遲時間縮小后更新模型，發現系統無死鎖。

8 相關工作

在層次擴展方面，Harel[15]通過擴展UML 狀態機圖提出了層次自動機的概念，解決了復雜系統狀態機規模大、層次嵌套深的問題，但嵌入式安全關鍵軟件的實時性描述仍然缺乏。為了解決時間自動機無法描述層次模型的問題，David[11]提出了層次時間自動機（HTA）的概念，并通過擴展時間自動機來解決復雜的層次系統建模和驗證問題。HTA可以建模分層系統并驗證它們的時間屬性，但它需要將模型手動轉換為自動機形式，這增加了工作的復雜性。

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

在混合建模方面，Ma 等人[22]使用高級建模語言AADL 進行系統架構設計；使用基于同步語言SIGNAL的形式化框架Polychrony進行分析和驗證。Yu等人[23]通過利用AADL 對嵌入式系統架構建模和利用Simulink對嵌入式系統功能建模，并通過形式化的多時鐘模型分析和驗證了系統的時間屬性。

9 總結與展望

本文通過擴展AADL 行為附件元模型的方式，對AADL功能行為描述能力進行了層次化擴展。通過提出層次行為附件（HBA）的方法，解決了建模過程中難以管理大量狀態以及結構層次丟失的問題。本文給出了層次行為附件的形式化語法約束以及形式化語義定義，通過對AADL 行為附件元模型的擴展，基于Xtext以及Xtend技術，在AADL開源開發環境OSATE上實現了對應的工具插件。為了便于形式化驗證，本文給出了HBA到時間自動機TA的轉換規則。最后，通過案例分析，驗證了方法的有效性。

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