基于NuSMV的AADL模型形式化驗證技術

劉暢，蔣永平，馬春燕,*，張濤

1.中國航空無線電電子研究所，上海 200233 2.西北工業大學 軟件學院，西安 710072

為保障任務關鍵系統的高可靠性需求，在軟件系統的設計階段對任務關鍵屬性進行形式化驗證是有效的技術手段之一。

AADL(Architecture Analysis and Design Language)是一種描述嵌入式系統架構的建模語言，在航空航天領域廣泛被應用。為在任務關鍵系統模型設計的早期階段，對AADL模型的任務關鍵屬性和系統行為的正確性進行驗證，NuSMV(New Symbolic Model Verifier)形式化模型發揮著重要的作用，NuSMV使用有限狀態機描述NuSMV模型，使用時態邏輯公式描述待驗證屬性，對相關屬性進行驗證。由于NuSMV工具的輸入語言支持以模塊化分層方式構建的復雜而龐大的系統，與AADL的層次化方式建立系統模型的思想一致。因此，可以通過將AADL模型轉換為NuSMV形式化模型，完成AADL模型的形式化驗證，如果驗證失敗，NuSMV會給出反例路徑，方便模型驗證人員快速定位問題來源，對模型進行優化。

目前已有多項研究將AADL模型轉化為形式化語言描述的模型，如LNT、Event-B、BIP、Maude、TASM及CSP等，然后對AADL模型的相關建模屬性進行正確性驗證。然而，這些工作僅考慮一個小的AADL子集，未涵蓋全部AADL軟構件以及相關行為、配置相關的建模要素，而這些關鍵的建模元素在模型的正確性驗證中較為常見。本文擬采用NuSMV對AADL模型的安全性和活性等屬性進行驗證。

1 相關工作

Mkaouar等介紹了一種AADL模型子集到LNT的轉換方法，通過CADP工具對系統并發正確性進行驗證。文獻[6]使用Event-B對AADL模型架構進行形式化驗證，但不包括行為模型的屬性驗證。本文研究團隊豐富了AADL行為模型及可調度性等驗證內容，采用Event-B對AADL模型進行形式化驗證。

Yang等將AADL轉換為抽象實時狀態機TASM，并基于定理證明器(Coq)對轉換的語義一致性進行驗證。劉倩等基于UPPAAL工具，對AADL模型可調度性進行分析，但其時間自動機模型不提供對時鐘的暫停及恢復，存在一定局限性。

Yang等使用可達自動機CSP構建AADL的形式化語義，并且使用FDR工具驗證死鎖和活鎖。文獻[13]使用HCSP構建AADL子集的形式化語義，并通過定理證明的方法驗證AADL模型行為附件的正確性。Zhang等介紹了一種從AADL模型到CSP的映射規則，并使用PAT(Process Analysis Toolkit)驗證AADL的安全性、活性等任務關鍵屬性。

文獻[15]將AADL轉換為NPTA(Networks of Priced Timed Automata)并且基于UPPAAL-SMC提出系統性能定性評估的方法。文獻[16]將AADL模型轉換為SIGNAL模型，并提供多時鐘約束的調度性分析。文獻[17]提出了利用NuSMV對AADL模型進行驗證的思想，但缺乏AADL模型到NuSMV模型的映射規則，以及采用NuSMV對AADL模型進行形式化驗證的系統化方法，僅通過一個案例說明如何利用NuSMV對AADL模型進行驗證。

對以上研究工作進行總結，可以發現前人方法存在以下3點不足。

1)部分研究工作考慮的AADL模型要素比較少，這樣會導致無法描述比較復雜的系統。

2)大部分研究工作沒有證明其方法的正確性，無法保證形式化模型與源模型語義一致。

3)模型系統待驗證屬性比較單一，局限性比較大。例如只支持LTL(Linear Temporal Logic)規范，這樣無法描述包含全稱和存在量詞的屬性。

為了彌補這些缺點，本文提出基于NuSMV的AADL模型驗證方法。

2 AADL和NuSMV

AADL是系統架構分析和設計語言，提供了系統和軟硬件構件以及構件之間交互關系的建模要素，AADL模型可以作為航空嵌入式系統的設計模型。AADL的軟件構件包含系統、子系統、進程、線程、線程組、數據和子程序，每個軟件構件都由類型和實現構成。AADL系統構件或軟件構件的任務級模態是其所包含的構件、連接和屬性值關聯的顯式配置，代表系統或軟件構件可選的操作狀態模態，模態配置也可以指定線程或子程序中要使用的不同調用序列，還可以表示在不同屬性值下的軟件構件(例如線程或子程序)的不同行為。系統或軟件構件行為的描述通過AADL行為附件(Behavior Annex)進行建模，例如描述構件的子程序調用、異步和時序等行為。

NuSMV是一套基于符號模型檢測技術的形式化建模語言和工具，用于有限狀態系統的形式化驗證，可以用于分析計算樹邏輯(CTL)和線性時序邏輯(LTL)表示的屬性，例如，安全性屬性和活性屬性。NuSMV程序由模塊(MODULE)構成，模塊定義由形參(Paramenter)和主體(Body)組成。模塊主體由描述狀態集Variables、轉移關系和對模型的一些約束Constraint、待驗證的規范Specification組成。

3 AADL模型到NuSMV模型的轉換方法

AADL模型到NuSMV模型的轉換方法的研究分為2個階段：確定需要轉換的AADL子集；建立從AADL模型子集到NuSMV模型子集的映射規則。

3.1 需要轉換的AADL子集

本文只考慮AADL模型的軟件構件(數據、子程序、線程、進程)和系統構件5種構件類型(component_type)，如表1所示。

圖1采用類圖展示了需要轉換的AADL模型建模要素及AADL構件的包含關系，系統構件可以包含系統構件、進程構件、子程序構件和數據構件，進程構件可以包含線程構件和數據構件，線程構件可以包含子程序構件和數據構件，子程序構件可以包含數據構件。表1中構件類型和構件子元素類型在圖1中用類名表示，構件子元素類型的構成要素用類的屬性表示。

表1 需要轉換的AADL子集Table 1 Subsets of AADL to be transformed

圖1 需要轉換的AADL建模要素Fig.1 AADL modeling elements needed to be con-verted

3.2 AADL模型到NuSMV模型的映射規則

映射規則是基于AADL元模型和NuSMV元模型提出來的。為了保證映射規則的完整性、以及一致性，每條映射規則都滿足從AADL元模型到NuSMV元模型節點的一對一映射，即每條映射規則都是同構映射。本節描述了AADL模型構件到NuSMV模塊的7類映射規則，分別對應構件類型及構件包含的6類子元素到NuSMV模型的映射規則。

圖2用UML類圖表示映射得到的NuSMV模型。AADL中的system、process、thread、subprogram和data構件分別映射為NuSMV中MODULE_main、MODULE_process、MODULE_thread、MODULE_subprogram和MODULE_data等5種類型的模塊(MODULE)，這些模塊均繼承MODULE_component，除了MODULE_data，其余4種模塊屬性一致，均包括多個MODULE_feature實例、多個MODULE_connection實例、一個枚舉類型的modes變量、多個枚舉類型的flow變量。NuSMV程序以main模塊作為驗證入口，main模塊對應AADL模型中的系統根節點。AADL構件的模態(modes)、數據流(flows)可以用NuSMV中的基本數據類型表示。

對本文提出的7類映射規則進行詳細闡釋，并結合算法1中的AADL進程構件MissionLoadP及其映射的NuSMV模塊為案例進行說明。

圖2 映射得到的NuSMV模型Fig.2 NuSMV model obtained by mapping

3.2.1 映射規則Rule1

Rule1表示根據AADL構件A的類型，將構件映射為NuSMV模塊A。如果構件A為系統構件，則映射為圖2中的main模塊(MODULE_main)；如果構件A為進程構件，則映射為MODULE_process，其他構件類型同理。圖3中的MissionLoadP進程構件映射為MissionLoadP模塊。

1) 進程模塊中的布爾變量isActive標記其在系統模態下是否有效。

2) 線程模塊中的布爾變量isBehavior標記線程組件在當前進程模態下是否執行其行為。

3) 進程模塊isActive變量的值隨著系統模塊模態切換而變換。線程模塊的isBehavior變量的值隨著進程模塊的模態切換而變換。

3.2.2 映射規則Rule2

構件A的features在表1中表示feature的集合。該集合中的每一個feature映射為一個feature MODULE實例，該實例會被connection模塊實例引用。特征模塊的定義如下：

MODULE feature(feaType,feaDirec)

DEFINE

Type:= feaType;

Direc:= feaDirec;

1) feaType 代表特征類型，AADL中定義的特征類型有抽象特征(Feature)、端口特征(Port)、參數特征(Parameter)、數據構件訪問特征(Data Access)。在轉換后的NuSMV模型中分別用1代表抽象特征(Feature)，2代表數據端口特征(Data Port)，3代表事件端口特征(Event Port)，4代表事件數據端口特征(Event Data Port)，5代表參數特征(Parameter)，6代表數據訪問特征(Data Access)。

算法1 AADL進程構件及其映射的NuSMV模塊

圖3 元模型和模型實例之間的映射關系Fig.3 Mappings between metamodels and models

2) feaDirec 代表特征方向，AADL中定義的特征方向有輸入(in)、輸出(out)、輸入輸出(in out)、提供(provides)、請求(requires)。本文在轉換之后的NuSMV模型中用-1代表輸入(in)、1代表輸出(out)、0代表輸入輸出(in out)、-2代表請求(requires)，2代表提供(provides)。

3) 如果構件的特征接口為事件端口特征(event port)或事件數據端口特征(event data port)，除了映射特征模塊實例，還需要在映射后的模塊中定義布爾類型變量，表示對應端口上的事件是否發生，該變量為TRUE代表事件到達，為FALSE代表事件未到達。該布爾類型變量可以作為模態轉換或行為狀態轉換的條件。

算法1中MissionLoadP進程特征“reqDispandControl: in event port”映射為MODULE MissionLoadP中的“reqDispandControl：feature(3,-1)”。

3.2.3 映射規則Rule3

每個子構件映射為一個MODULE實例，所有子構件映射的MODULE實例均會被MODULE A引用。如果subcomponent_name是AADL構件A的某一個子構件的名字，component_type是子構件的類型，則映射的MODULE實例名為subcomponent_name，映射的MODULE實例的類型為component_type。

算法1中的MissionLoadP進程構件包含線程子構件getLocalPlaneAttributeInfo。線程子構件在模塊MissionLoadP中表示為getInfo： getLocalPlaneAttributeInfo()。

3.2.4 映射規則Rule4

構件A的connections在表1中表示connection的集合，該集合中的每一條connection映射為connection MODULE實例。該實例會被模塊A引用，連接模塊的定義如下：

MODULE connection(src_feature,dst_feature,conn_type)

VAR

isWorking： boolean;

1) src_feature 對應連接的源特征，其類型為特征模塊(即MODULE_feature)。

2) dst_feature 代表連接的目的特征，其類型為特征模塊(即MODULE_feature)。

3) connType 代表連接類型，分為同級構件相連的連接類型、構件到子構件的連接類型及構件到父構件的連接類型，本文在NuSMV中分別用0、-1、1表示。

4) isWorking用以驗證該連接在的模態下是否有效，其默認值為TRUE。

算法1中的“conn1:port getInfo.outport→returnPlaneInfo”映射為“conn1:connection(getInfo.outport,returnPlaneInfo,1)”，getInfo.outport為源特征，returnPlaneInfo為目的特征，1表示構件MissionLoadP的子構件端口到該構件端口的連接。

3.2.5 映射規則Rule5

構件A的modes在表1中表示modes子元素類型，其映射為枚舉類型的modes變量，例如，該枚舉變量表示為modes:{mode1, mode2, mode3}，其中，mode1、mode2、mode3對應表1中modes子元素類型的構成要素modes_set。算法1中的進程MissionLoadP的modes的轉換，枚舉值對應構件所有的操作狀態，模態之間的轉移關系用NuSMV中的next()表達式和case語句表示。

3.2.6 映射規則Rule6

構件A的behavior_annex在表1中表示behavior_annex子元素類型，映射為一個behavior MODULE實例，例如算法1中的線程getLocalPlaneAttributeInfo 行為附件的轉換滿足以下映射規則：

1)行為附件中的變量(variables)轉換為NuSMV模塊中的變量聲明。

2)行為附件的狀態集合(states)轉換為NuSMV模塊中枚舉類型的變量聲明。NuSMV模塊中states變量的枚舉值對應行為附件中定義的狀態，包括initial狀態、complete狀態、final狀態和execution狀態。

3)行為附件中的復合狀態被分解為多個原子狀態。比如s0為initial和complete的一個復合狀態，轉換成s0_initial和s0_complete 2個狀態。

4)行為附件的轉移關系(transitions)映射為NuSMV的next(states)函數和case語句，描述AADL行為中行為狀態的轉移關系。

3.2.7 映射規則Rule7

構件A的flows在表1中表示flow的集合，該集合中的每一個flow映射為一個枚舉類型變量，例如AADL中flow映射為NuSMV中枚舉變量： flow: {feature,feature,…,feature}，其中，feature,feature,…,feature對應流s1經過的個特征集合。流的轉移關系用NuSMV中的next()表達式和case語句表示，例如，算法1中從getLocalPlaneAttributeInfo線程的端口和進程MissionLoadP的端口形成的流s3到NuSMV模型的轉換體現了該映射規則。

3.3 NuSMV模型的生成算法

基于上述7條規則的NuSMV模型生成算法如算法2所示。該算法以AADL模型構件為輸入，以生成的NuSMV模塊為輸出，create表示生成NuSMV元素，VAR表示生成NuSMV變量，ASSIGN表示生成變量的轉移關系，next(var)表示用NuSMV中的next語句描述var的轉移關系。

算法2描述了AADL構件的NuSMV模型生成方法。該算法的輸入為AADL語言表示的構件A，構件A的生成方法分為以下8步：

算法2 NuSMV模型生成算法

1) 首先根據構件A的構件類型生成對應的NuSMV模塊，按照映射規則Rule1,如果是system，則創建MODULE_main，否則生成MODULE_component_name，如算法2的第1～5行所示。

2) 然后根據構件A包含的子元素類型，生成對應的NuSMV元素。如算法2的第6～50行所示。

3) 如果構件A包含features，按照映射規則Rule2生成每個feature對應的feature_MODULE實例，如算法2的第8～12行所示。

4) 如果構件A包含subcomponents，按照映射規則Rule3生成每個subcomponent對應的MODULE實例，如算法2的第13～23行所示。

5) 如果構件A包含connections，按照映射規則Rule4生成每個connection對應的connection MODULE實例，如算法2的第24～31行所示。

6) 如果構件A包含modes，按照映射規則Rule5生成modes變量，如算法2的第32～34行所示。

7) 如果構件A包含behavior_annex，按照映射規則Rule6生成behavior MODULE實例，如算法2的第35～42行所示。

8) 如果構件A包含flows，按照映射規則Rule7生成每個flow對應的枚舉類型變量，如算法2的第43～49行所示。

4 AADL模型到NuSMV模型轉換方法的正確性證明

模型轉換的正確性表現為映射規則滿足AADL語義保留、確定性以及有限性等性質。本采取圖同構的方法對本文模型轉換方法的正確性進行驗證。

本文的轉換方法是基于AADL元模型和NuSMV元模型提出的，AADL元模型中的節點要素到NuSMV元模型中的節點要素是一一對應的，滿足圖同構的定義。本文通過證明轉換后的NuSMV模型實例與源AADL模型實例語義一致，說明AADL模型到NuSMV轉換方法的正確性。證明思路如圖3所示。

圖3表示元模型和模型實例之間的映射關系，其中Ins(MMt)指目標語言的模型實例；表示源語言元模型到目標語言源模型的轉換；表示源語言模型實例到目標語言模型實例之間的映射；、′分別表示源語言和目標語言元模型到模型實例之間的映射；表示源語言元模型到目標模型實例之間的映射關系；MMs表示AADL元模型；MMt表示NuSMV的元模型。映射函數和′為類型保留映射 (Type Prserve Mapping,TPM),TPM由OMG(Object Management Group)定義。

由3.1節可知，根據提出的AADL元模型和NuSMV元模型類圖之間的同構映射，映射函數是圖同構的。本節將證明AADL元模型與其模型實例Ins(MM)之間的類型保留映射函數是圖同構的，同時證明(°)是圖同構的，在此基礎上證明AADL模型實例到NuSMV模型實例的模型轉換函數是圖同構的。

定義一個圖同構函數表示圖從圖到圖的轉換：=(:→,:→),其中，為圖的節點集合；為圖節點到圖節點集合的映射函數;為圖的節點集合;為圖邊緣節點集合到圖邊緣節點集合的映射函數；為圖的邊緣節點集合；為圖的邊緣節點集合。滿足以下約束:

(1)

式中：、分別為同時作用于圖的節點和邊緣節點的轉換函數。

元模型MM為一個UML(Unified Modeling Language)類圖，Ins(MM)為一個UML對象圖。TPM函數從MM映射為Ins(MM)，Ins(MM)中的每一個元素都是MM中類的映射。

如果元模型MM為UML類圖，模型實例Ins(MM)為UML對象圖。那么在元模型圖及其實例圖之間定義的TPM函數是圖同構的。

根據命題1，在AADL元模型類圖到NuSMV元模型類圖的轉換中，因為AADL元模型元素到其模型實例元素之間，以及NuSMV元模型元素到其模型實例之間的映射都是類型保留映射TPM，所以映射函數和′是圖同構的。

如果映射函數是圖同構的，并且映射函數是圖同構的，那么和的組合°也是圖同構的。

根據命題2，因為函數、是圖同構的，所以(°)是圖同構的。

已知在元模型MM和MM′之間存在同構映射，元模型MM和它的實例Ins(MM)之間存在類型保留映射函數，元模型MM′和它的實例Ins(MM′)之間存在類型保留映射函數′，則Ins(MM)和Ins(MM′)之間的映射函數是圖同構的。

如圖3所示，上文已經證明函數、、′、都是圖同構的，分別用式(2)～式(5)表示

(MM)=MM’′是圖同構

(2)

(MM)=Ins(MM)是圖同構

(3)

(MM)=Ins(MM′)是圖同構

(4)

(MM)=′((MM))=Ins(MM′)是圖同構的

(5)

根據定義1和式(2)，可得

(6)

根據定義1和式(5)，可得

(7)

假設如圖3所示，=°，將式(7)中的替換成°，可得

(8)

根據式(8)，因為是圖同構的，結合定義1的約束，據此推斷映射函數也是圖同構的。

本轉換方法是基于源模型和目標模型的語法結構以及源模型語義角度提出的。基于源模型和目標模型的語法結構采用上下文無關文法描述，是精確無二義性的，所以模型轉換為一對一映射，是確定的。同時AADL模型的構成要素是有限的，因此轉換方法是有限的。

綜上，證明了本文從AADL模型至NuSMV模型轉換方法的正確性。

5 基于NuSMV模型的驗證方法

5.1 安全屬性的驗證

本文驗證的安全屬性(Safety)包括狀態、模態的可達性和轉換的確定性。

5.1.1 可達性驗證

在狀態遷移系統中，如果事件或者消息到達指定端口，將會切換為另一個狀態。狀態的可達性驗證指在所有可能的狀態轉換序列中，是否存在目標狀態不可達的情況。

1) 模態可達性驗證

模態的可達性指當事件數據端口上有事件到達時，一個模態能夠轉換為另一個模態的能力。例如，圖4(a)展示了一個由于模態3沒有傳出轉換導致的非可達性示例，圖4(b)展示了一個滿足模態可達性的示例。對于圖4，在NuSMV中，表示是否存在從mode1到mode3的模態轉換序列，模態可達性的CTL描述為

AG(modes=mode1→AF(modes=mode3))

(9)

2) 行為附件狀態可達性驗證

行為附件狀態的可達性指衛式(Guard)滿足時，從一個行為狀態切換到另一個行為狀態的能力，衛式是指狀態轉換時滿足的約束條件。例如，圖5(a)表示由于s1和s2沒有傳出轉換，所以從s2到s1，或從s1到s2都是不可達的；圖5(b) 表示了一個狀態可達的案例。在NuSMV中，表示是否存在從s1到s2的行為狀態轉換序列，行為附件狀態的可達性CTL描述為

AG((states=s1) →AF(states=s2))

(10)

圖4 模態可達性示例Fig.4 Example of mode reachability

圖5 行為狀態可達性Fig.5 Example of state reachability

5.1.2 確定性驗證

狀態轉換分為確定性和非確定性。在一個狀態上，對于同一個轉換條件，有且只有一條轉換，則稱該轉換是確定性的，否則為非確定性的。AADL模型中的模態和行為狀態轉換必須是確定性的。例如，圖6(a)所示為當port1上的事件到達時，模態會從mode1向mode2轉換，或向mode3轉換，這屬于非確定性的模態轉換；圖6(b) 所示為確定性的模態轉換案例，對每一個源模態，每一個轉換條件只存在唯一的傳出轉換。NuSMV表示到mode2模態的轉換是否是確定性的，對應的CTL規范描述為

AF modes = mode2

(11)

圖6 模態轉換的確定性Fig.6 Example of deterministic mode transition

5.2 活性屬性的驗證

活性屬性指“計劃的事情最終一定會發生”。活性屬性驗證包括進度屬性的驗證。進度屬性指“如果滿足某些條件，某些事情最終一定會發生”。AADL模態切換、行為附件中行為狀態的切換皆定義了進度屬性。NuSMV中，如果模態切換的條件(Event)滿足，模態將會按照計劃切換為mode2，模態進度屬性的CTL規范描述為：AG(event →AF(modes=mode2))；如果行為狀態轉換的條件滿足，行為狀態將會按照計劃變成S0狀態，行為附件中行為狀態的進度屬性對應的CTL規范描述為

AG(event → AF(states=S0))

(12)

5.3 模態配置的合法性驗證

AADL模型中，構件對其所包含的子構件、連接等元素與模態的關聯性進行配置，表示不同操作狀態下的構件行為。本文對模態配置的合法性驗證包括連接元素模態配置的合法性驗證、子構件模態配置的合法性驗證、流元素模態配置的合法性驗證及系統構件下線程行為嵌套配置的合法性驗證4部分。

1) 連接元素模態配置的合法性驗證

AADL模型中連接表示不同構件之間的數據交互，連接元素模態配置的合法性指構件間的數據交互是否符合模態配置的要求。NuSMV中，conn1只在模態mode1下有效的性質對應的CTL規范描述為

A[!conn1.is Working U modes=mode1]

(13)

2) 子構件模態配置的合法性驗證

AADL模型中，不同的模態指定了構件不同的操作狀態。子構件模態配置的合法性指子構件的有效性是否符合構件模態配置的要求。映射規則Rule1中提到，進程模塊的isActive屬性標識進程模塊是否在系統模塊的模態配置下有效；線程模塊的isBehavior屬性標識線程模塊是否在進程模塊的模態配置下有效。NuSMV中，表示進程模塊p在系統模態mode1下是否有效的CTL規范描述為

AF(modes=mode1 & p.is Active)

(14)

3) 流元素模態配置的合法性驗證

AADL模型中，因為流元素的合法性與連接的合法性及子構件的合法性有關。所以流的可達性與模態配置具有一定的關聯關系。

NuSMV中，表示在模態mode1下，流flow是否可以達到指定的特征接口，流元素模態配置的合法性屬性對應的CTL規范描述為

AG(modes=mode1)→AF(flow=feature))

(15)

4) 系統構件下線程行為模態嵌套的合法性驗證

AADL模型中，系統構件的模態配置影響進程構件的有效性，進程構件的模態配置影響線程子構件的行為執行。所以系統構件的模態配置，會間接對具體線程的行為執行產生影響。

系統構件下線程行為配置的合法性驗證就是判斷線程行為的有效性是否符合系統定義的模態配置。NuSMV中，表示在系統模態mode2下，進程構件p中的線程構件t是否能夠正常執行，該性質對應的CTL規范描述為

AF(modes=mode2 & p.t.is Behavior)

(16)

6 實驗驗證

以包含人機交互子系統、備份子系統和自動飛行子系統的飛行控制系統為例，詳細闡釋了基于NuSMV的AADL模型形式化驗證方法。

6.1 實驗案例

人機交互子系統負責處理飛行員對飛機的操作指令，并且負責顯示飛機的各項飛行參數。該子系統包含了顯示控制進程和飛行員輸入進程。顯示進程將飛機的飛行參數展示給飛行員，并且根據飛行員的操作控制駕駛桿、油門桿和周邊鍵等設備。飛行員輸入進程包含3個分別處于不同計算機上的飛行員輸入線程，當1個輸入線程發生異常時，會由其他飛行員輸入線程完成對飛行員輸入信息的處理。

備份子系統的主要功能為備份重要的數據信息，當飛行控制系統發生異常狀況時，能夠根據備份信息恢復正常，備份子系統運行在PowerPC_G4處理器上。

自動飛行子系統主要功能為讀取GPS(Global Positioning System)數據，發送控制信號至控制平臺實現飛機的自動飛行，該子系統包括GPS讀取線程以及自動導航線程。GPS讀取線程僅在初始狀態從GPS讀取飛機位置信息，當開啟自動駕駛后，自動導航線程開始運行，飛機進入自動駕駛狀態。

6.2 實驗案例——飛行控制系統的AADL模型

使用OSATE工具為飛行控制系統建模。該AADL模型包括人機交互子系統S_HCI、自動飛行子系統S_NAP和備份子系統S_BUP。

S_HCI包含1個飛行員輸入進程構件P_Pinput和1個顯示控制進程構件P_DIS，表示駕駛桿、油門桿和周邊鍵的設備構件以及表示線程運行平臺的處理器構件。P_Pinput包含3個綁定到不同處理器的飛行員輸入線程T_Pilot_Input1、T_Pilot_Input2、T_Pilot_Input3。同時P_Pinput包含3個輸入線程的模態配置，表示不同情況下不同線程的執行情況。飛行員輸入線程為后臺線程，當飛行員輸入命令的時候會啟動。P_DIS包括2個線程構件顯示線程T_Screen_Disp和設備控制線程T_Control_Dev。顯示線程每50 ms會刷新界面顯示，設備控制線程根據飛行員輸入信息控制駕駛桿、油門桿和周邊鍵3個設備。

S_NAP中有2個模態：加載(load)和執行(run)。當自動飛行子系統接收到自動駕駛打開的事件，模態會由load變為run。導航控制進程P_Nav_Con只在run模態下正常執行。P_Nav_Con包含GPS讀取線程T_GPS_Reader和自動導航計算線程T_AP_Compute，該進程構件有3種工作模態，即:GPS打開及自動導航關閉模態GPS_UP_AP_DOWN、GPS打開及自動導航打開模態GPS_UP_AP_UP、GPS關閉模態GPS_DOWN。如果GPS出現故障時，飛行控制系統不能自動飛行。

S_BUP包含1個備份進程構件P_BUP和PowerPC_G4處理器構件，P_BUP包含1個數據庫訪問線程構件T_DB_Operation，主要負責訪問數據庫中的備份信息，該線程構件與PowerPC_G4處理器構件的關系通過S_BUP子系統構件的Actual_Processor_Binding屬性表示。

當導航控制進程處在GPS_UP_AP_DOWN模態時，如果飛行員將飛機駕駛狀態調整為自動駕駛，則模態會變成GPS_UP_AP_UP模態，如果GPS發生故障，模態將會變成GPS_DOWN模態。T_GPS_Reader線程在GPS_UP_AP_DOWN和GPS_UP_AP_UP模態下都可以正常工作。該線程每隔20 ms從GPS獲取一次數據。T_AP_Compute線程僅在GPS_UP_AP_UP模態下正常工作，該線程每隔50 ms會輸出一次飛機的俯仰角、偏航角、滾動角信息給制動器，以實現飛機自動導航。

6.3 生成的實驗案例——飛行控制系統的NuSMV模型

基于AADL模型到NuSMV模型的映射規則和轉換算法，構建飛行控制系統的NuSMV模型。NuSMV模型包括：1個main模塊，S_HCI、S_NAP和S_BUP 3個子系統模塊,P_Pinput、P_DIS、P_BUP和P_Nav_Con 4個進程模塊,T_Pilot_Input1、T_Pilot_In put 2、T_Polot_Input 3、T_Screen_Disp、T_Control_Dev、T_DB_Operation、T_GPS_Reader和T_AP_Compute 8個線程模塊以及表示線程模塊行為的行為附件模塊；3個數據模塊。例如，生成的P_Nav_Con進程模塊(導航控制進程)如算法3所示，其中modes變量的轉移關系如算法4所示，T_GPS_Reader線程模塊及其行為附件模塊如算法5所示。

算法3 導航控制進程模塊

算法4 modes變量的轉換關系

算法5 線程模塊及其行為附件模塊Algorithm 5 Thread module and behavior_annex module

6.4 實驗案例——飛行控制系統的形式化驗證

基于飛行控制系統NuSMV形式化模型，對其安全屬性、活性屬性以及模態配置的合法性進行驗證，如果相應屬性的驗證結果為TRUE，則表示驗證屬性符合要求;否則NuSMV會給出一條反例路徑，說明驗證失敗的原因，模型驗證人員可以根據反例路徑去完善建模方案。

6.4.1 安全屬性的驗證

安全屬性驗證包括可達性及確定性的驗證。

1)可達性驗證

①Nav_Control_Process模塊modes的可達性驗證

如果當前模態為GPS_UP_AP_DOWN，驗證GPS_UP_AP_UP是否可達，該屬性對應的CTL規范為

AG(modes=GPS_UP_AP_DOWN→

AF(modes=GPS_UP_AP_UP))

(17)

驗證結果為TRUE表示Nav_Control_Process進程的GPS_UP_AP_UP模態滿足從GPS_UP_AP_DOWN模態開始的可達性，否則模型存在故障。

② T_GPS_Reader行為狀態的可達性驗證

T_GPS_Reader的行為附件的reader1狀態表示該線程調度完成，驗證reader1行為狀態是否可達。該屬性對應的CTL規范為

AG(states=reader0→EF(states=reader1))

(18)

驗證結果為TRUE表示T_GPS_Reader可以被正常調度，否則存在故障。

2)確定性驗證。

對Nav_Control_Process的GPS_DOWN模態進行確定性方面的驗證，模態的確定性保證了構件不同的操作行為都可以正常執行。該屬性對應的CTL規范為

AF modes=GPS_DOWN

(19)

驗證結果為FALSE，對NuSMV工具給出的反例路徑進行查看，發現如果GPS_error事件一直未發生，進程模態就不會變成GPS_DOWN。在實際情況中，GPS錯誤事件有一定概率發生，這是由于未添加公平性約束導致的驗證結果與預期不符。對GPS_error變量添加公平性約束并重新驗證，模型滿足該條屬性。

6.4.2 活性屬性的驗證

1) Nav_Control_Process的GPS_UP_AP_UP模態的活性驗證

GPS_UP_AP_UP表示GPS打開及自動導航打開模態，當人機交互子系統設置飛機為自動駕駛狀態時，導航控制進程會接收到自動導航指令，工作模態也會變成GPS_UP_AP_UP。該屬性對應的CTL規范為

AG(AP_Toggle_event→AF(modes=

GPS_UP_AP_UP))

(20)

驗證結果為TRUE表示一旦飛行員設置飛機飛行狀態為自動駕駛，Nav_Control_Process進程會在GPS打開及自動導航打開(GPS_UP_AP_UP)模態下執行。

2) T_GPS_Reader行為狀態的活性屬性驗證

當T_GPS_Reader接收到改變駕駛狀態的消息時，T_GPS_Reader會自動獲取飛機位置信息。該屬性對應的CTL規范為

AG(AP_Position_Input_event→AF(behavior_

specification.states=reader1))

(21)

驗證結果為TRUE表示T_GPS_Reader線程只要接收到改變駕駛狀態的消息時，總會成功執行其行為；否則模型存在故障。

6.4.3 模態配置的合法性驗證

1) 連接元素模態配置的合法性驗證

當Nav_Control_Process以GPS_UP_AP_UP模態工作時，與自動導航計算線程T_AP_Compute線程有關的連接應該是有效的。該屬性對應的CTL規范為

A[!conn1.is Working U modes=

GPS_UP_AP_UP]

(22)

驗證結果為TRUE表示在模態為GPS_UP_AP_UP時，連接conn1總是有效的，否則存在故障。

2) 子構件模態配置的合法性驗證

T_AP_Compute僅在GPS_UP_AP_UP模態下才正常執行。該屬性對應的CTL規范為

AF(modes=GPS_UP_AP_UP &

T_AP_Compute.is Behavior)

(23)

驗證結果為TRUE表示T_AP_Compute符合Nav_Control_Process的模態配置定義，僅在GPS_UP_AP_UP模態下執行，否則存在故障。

3) 流元素模態配置的合法性驗證

AADL模型中定義的數據流data，只有在模態GPS_UP_AP_UP下，才可以到達滾動角輸出接口(Delta_Roll_Output)。該屬性對應的CTL規范為

AG(modes=GPS_UP_AP_UP→AF(data=

Delta_Roll_Output))

(24)

驗證結果為TRUE表示在GPS_UP_AP_UP模態下，流data總能達到滾動角輸出接口，即流的有效性符合Nav_Control_Process的模態配置定義，否則存在故障。

4) 系統構件下線程行為配置的合法性驗證Nav_Control_Process進程僅在自動飛行子系統模態為run時，才會正常執行。而Nav_Control_Process內的T_AP_Compute線程僅在進程模態為GPS_UP_AP_UP時，才會執行。驗證系統模態為run模態時，T_AP_Compute線程是否會正常執行。該屬性對應的CTL規范為

AF (modes=run & Nav_Control_Process.

T_AP_Compute.is Behavior)

(25)

驗證結果為TRUE表示T_AP_Compute的行為符合系統模態的配置定義，否則存在故障。

6.5 驗證結果分析

通過在AADL模型中插入10種故障類型，形成不同的AADL故障設計模型，并對其進行驗證，均可以發現相應的故障，證明了本文方法的有效性。通過對飛行控制系統的驗證結果進行分析，實驗結果統計信息(包括故障說明、驗證故障數目、驗證故障總數、驗證消耗時間和空間)如表2 所示。

表3展示了本文提出的基于NuSMV的AADL模型形式化驗證方法與其他方法的對比結果，通過對比，本文方法主要具有以下3個方面的優勢:

1) 考慮的AADL子集更豐富，包括構件、特征、連接、模態、數據流及行為附件等建模元素。

2) 采用圖同構的方法保留AADL模型語義，以保證AADL模型到NuSMV模型轉換的正確性、有效性和有限性。

3) 對AADL模型中的安全性、活性、模態配置的正確性進行驗證，其中模態配置驗證包括連接子元素、子構件及流元素的模態配置，以及系統層次化建模導致的模態嵌套正確性的驗證。

7 結 論

本文覆蓋了全部AADL軟構件、系統和構件行為、模態配置和模態嵌套相關的建模要素，提出了一種基于NuSMV的AADL模型形式化驗證方法，以驗證AADL模型中安全性、活性和任務屬性配置模態的正確性。由于NuSMV自身的缺陷，部分屬性無法驗證，比如模型精化屬性、可調度性。所以本文與團隊之前發表的文獻[7]分別使用2種形式化方法對AADL模型進行驗證，兩種方法的側重點不同，具有互補性。

表2 實驗結果統計信息Table 2 Statistics of experimental results

表3 相關工作比較Table 3 Comparison of related works

續表3