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

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

為保障任務(wù)關(guān)鍵系統(tǒng)的高可靠性需求，在軟件系統(tǒng)的設(shè)計階段對任務(wù)關(guān)鍵屬性進行形式化驗證是有效的技術(shù)手段之一。

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

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

1 相關(guān)工作

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

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

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

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

對以上研究工作進行總結(jié)，可以發(fā)現(xiàn)前人方法存在以下3點不足。

1)部分研究工作考慮的AADL模型要素比較少，這樣會導(dǎo)致無法描述比較復(fù)雜的系統(tǒng)。

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

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

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

2 AADL和NuSMV

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

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

3 AADL模型到NuSMV模型的轉(zhuǎn)換方法

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

3.1 需要轉(zhuǎn)換的AADL子集

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

圖1采用類圖展示了需要轉(zhuǎn)換的AADL模型建模要素及AADL構(gòu)件的包含關(guān)系，系統(tǒng)構(gòu)件可以包含系統(tǒng)構(gòu)件、進程構(gòu)件、子程序構(gòu)件和數(shù)據(jù)構(gòu)件，進程構(gòu)件可以包含線程構(gòu)件和數(shù)據(jù)構(gòu)件，線程構(gòu)件可以包含子程序構(gòu)件和數(shù)據(jù)構(gòu)件，子程序構(gòu)件可以包含數(shù)據(jù)構(gòu)件。表1中構(gòu)件類型和構(gòu)件子元素類型在圖1中用類名表示，構(gòu)件子元素類型的構(gòu)成要素用類的屬性表示。

表1 需要轉(zhuǎn)換的AADL子集Table 1 Subsets of AADL to be transformed

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

3.2 AADL模型到NuSMV模型的映射規(guī)則

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

圖2用UML類圖表示映射得到的NuSMV模型。AADL中的system、process、thread、subprogram和data構(gòu)件分別映射為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模塊對應(yīng)AADL模型中的系統(tǒng)根節(jié)點。AADL構(gòu)件的模態(tài)(modes)、數(shù)據(jù)流(flows)可以用NuSMV中的基本數(shù)據(jù)類型表示。

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

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

3.2.1 映射規(guī)則Rule1

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

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

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

3) 進程模塊isActive變量的值隨著系統(tǒng)模塊模態(tài)切換而變換。線程模塊的isBehavior變量的值隨著進程模塊的模態(tài)切換而變換。

3.2.2 映射規(guī)則Rule2

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

MODULE feature(feaType,feaDirec)

DEFINE

Type:= feaType;

Direc:= feaDirec;

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

算法1 AADL進程構(gòu)件及其映射的NuSMV模塊

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

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

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

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

3.2.3 映射規(guī)則Rule3

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

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

3.2.4 映射規(guī)則Rule4

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

MODULE connection(src_feature,dst_feature,conn_type)

VAR

isWorking： boolean;

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

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

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

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

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

3.2.5 映射規(guī)則Rule5

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

3.2.6 映射規(guī)則Rule6

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

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

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

3)行為附件中的復(fù)合狀態(tài)被分解為多個原子狀態(tài)。比如s0為initial和complete的一個復(fù)合狀態(tài)，轉(zhuǎn)換成s0_initial和s0_complete 2個狀態(tài)。

4)行為附件的轉(zhuǎn)移關(guān)系(transitions)映射為NuSMV的next(states)函數(shù)和case語句，描述AADL行為中行為狀態(tài)的轉(zhuǎn)移關(guān)系。

3.2.7 映射規(guī)則Rule7

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

3.3 NuSMV模型的生成算法

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

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

算法2 NuSMV模型生成算法

1) 首先根據(jù)構(gòu)件A的構(gòu)件類型生成對應(yīng)的NuSMV模塊，按照映射規(guī)則Rule1,如果是system，則創(chuàng)建MODULE_main，否則生成MODULE_component_name，如算法2的第1～5行所示。

2) 然后根據(jù)構(gòu)件A包含的子元素類型，生成對應(yīng)的NuSMV元素。如算法2的第6～50行所示。

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

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

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

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

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

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

4 AADL模型到NuSMV模型轉(zhuǎn)換方法的正確性證明

模型轉(zhuǎn)換的正確性表現(xiàn)為映射規(guī)則滿足AADL語義保留、確定性以及有限性等性質(zhì)。本采取圖同構(gòu)的方法對本文模型轉(zhuǎn)換方法的正確性進行驗證。

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

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

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

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

(1)

式中：、分別為同時作用于圖的節(jié)點和邊緣節(jié)點的轉(zhuǎn)換函數(shù)。

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

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

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

如果映射函數(shù)是圖同構(gòu)的，并且映射函數(shù)是圖同構(gòu)的，那么和的組合°也是圖同構(gòu)的。

根據(jù)命題2，因為函數(shù)、是圖同構(gòu)的，所以(°)是圖同構(gòu)的。

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

如圖3所示，上文已經(jīng)證明函數(shù)、、′、都是圖同構(gòu)的，分別用式(2)～式(5)表示

(MM)=MM’′是圖同構(gòu)

(2)

(MM)=Ins(MM)是圖同構(gòu)

(3)

(MM)=Ins(MM′)是圖同構(gòu)

(4)

(MM)=′((MM))=Ins(MM′)是圖同構(gòu)的

(5)

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

(6)

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

(7)

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

(8)

根據(jù)式(8)，因為是圖同構(gòu)的，結(jié)合定義1的約束，據(jù)此推斷映射函數(shù)也是圖同構(gòu)的。

本轉(zhuǎn)換方法是基于源模型和目標模型的語法結(jié)構(gòu)以及源模型語義角度提出的?；谠茨Ｐ秃湍繕四Ｐ偷恼Z法結(jié)構(gòu)采用上下文無關(guān)文法描述，是精確無二義性的，所以模型轉(zhuǎn)換為一對一映射，是確定的。同時AADL模型的構(gòu)成要素是有限的，因此轉(zhuǎn)換方法是有限的。

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

5 基于NuSMV模型的驗證方法

5.1 安全屬性的驗證

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

5.1.1 可達性驗證

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

1) 模態(tài)可達性驗證

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

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

(9)

2) 行為附件狀態(tài)可達性驗證

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

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

(10)

圖4 模態(tài)可達性示例Fig.4 Example of mode reachability

圖5 行為狀態(tài)可達性Fig.5 Example of state reachability

5.1.2 確定性驗證

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

AF modes = mode2

(11)

圖6 模態(tài)轉(zhuǎn)換的確定性Fig.6 Example of deterministic mode transition

5.2 活性屬性的驗證

活性屬性指“計劃的事情最終一定會發(fā)生”?；钚詫傩则炞C包括進度屬性的驗證。進度屬性指“如果滿足某些條件，某些事情最終一定會發(fā)生”。AADL模態(tài)切換、行為附件中行為狀態(tài)的切換皆定義了進度屬性。NuSMV中，如果模態(tài)切換的條件(Event)滿足，模態(tài)將會按照計劃切換為mode2，模態(tài)進度屬性的CTL規(guī)范描述為：AG(event →AF(modes=mode2))；如果行為狀態(tài)轉(zhuǎn)換的條件滿足，行為狀態(tài)將會按照計劃變成S0狀態(tài)，行為附件中行為狀態(tài)的進度屬性對應(yīng)的CTL規(guī)范描述為

AG(event → AF(states=S0))

(12)

5.3 模態(tài)配置的合法性驗證

AADL模型中，構(gòu)件對其所包含的子構(gòu)件、連接等元素與模態(tài)的關(guān)聯(lián)性進行配置，表示不同操作狀態(tài)下的構(gòu)件行為。本文對模態(tài)配置的合法性驗證包括連接元素模態(tài)配置的合法性驗證、子構(gòu)件模態(tài)配置的合法性驗證、流元素模態(tài)配置的合法性驗證及系統(tǒng)構(gòu)件下線程行為嵌套配置的合法性驗證4部分。

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

AADL模型中連接表示不同構(gòu)件之間的數(shù)據(jù)交互，連接元素模態(tài)配置的合法性指構(gòu)件間的數(shù)據(jù)交互是否符合模態(tài)配置的要求。NuSMV中，conn1只在模態(tài)mode1下有效的性質(zhì)對應(yīng)的CTL規(guī)范描述為

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

(13)

2) 子構(gòu)件模態(tài)配置的合法性驗證

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

AF(modes=mode1 & p.is Active)

(14)

3) 流元素模態(tài)配置的合法性驗證

AADL模型中，因為流元素的合法性與連接的合法性及子構(gòu)件的合法性有關(guān)。所以流的可達性與模態(tài)配置具有一定的關(guān)聯(lián)關(guān)系。

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

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

(15)

4) 系統(tǒng)構(gòu)件下線程行為模態(tài)嵌套的合法性驗證

AADL模型中，系統(tǒng)構(gòu)件的模態(tài)配置影響進程構(gòu)件的有效性，進程構(gòu)件的模態(tài)配置影響線程子構(gòu)件的行為執(zhí)行。所以系統(tǒng)構(gòu)件的模態(tài)配置，會間接對具體線程的行為執(zhí)行產(chǎn)生影響。

系統(tǒng)構(gòu)件下線程行為配置的合法性驗證就是判斷線程行為的有效性是否符合系統(tǒng)定義的模態(tài)配置。NuSMV中，表示在系統(tǒng)模態(tài)mode2下，進程構(gòu)件p中的線程構(gòu)件t是否能夠正常執(zhí)行，該性質(zhì)對應(yīng)的CTL規(guī)范描述為

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

(16)

6 實驗驗證

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

6.1 實驗案例

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

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

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

6.2 實驗案例——飛行控制系統(tǒng)的AADL模型

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

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

S_NAP中有2個模態(tài)：加載(load)和執(zhí)行(run)。當自動飛行子系統(tǒng)接收到自動駕駛打開的事件，模態(tài)會由load變?yōu)閞un。導(dǎo)航控制進程P_Nav_Con只在run模態(tài)下正常執(zhí)行。P_Nav_Con包含GPS讀取線程T_GPS_Reader和自動導(dǎo)航計算線程T_AP_Compute，該進程構(gòu)件有3種工作模態(tài)，即:GPS打開及自動導(dǎo)航關(guān)閉模態(tài)GPS_UP_AP_DOWN、GPS打開及自動導(dǎo)航打開模態(tài)GPS_UP_AP_UP、GPS關(guān)閉模態(tài)GPS_DOWN。如果GPS出現(xiàn)故障時，飛行控制系統(tǒng)不能自動飛行。

S_BUP包含1個備份進程構(gòu)件P_BUP和PowerPC_G4處理器構(gòu)件，P_BUP包含1個數(shù)據(jù)庫訪問線程構(gòu)件T_DB_Operation，主要負責(zé)訪問數(shù)據(jù)庫中的備份信息，該線程構(gòu)件與PowerPC_G4處理器構(gòu)件的關(guān)系通過S_BUP子系統(tǒng)構(gòu)件的Actual_Processor_Binding屬性表示。

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

6.3 生成的實驗案例——飛行控制系統(tǒng)的NuSMV模型

基于AADL模型到NuSMV模型的映射規(guī)則和轉(zhuǎn)換算法，構(gòu)建飛行控制系統(tǒng)的NuSMV模型。NuSMV模型包括：1個main模塊，S_HCI、S_NAP和S_BUP 3個子系統(tǒng)模塊,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個數(shù)據(jù)模塊。例如，生成的P_Nav_Con進程模塊(導(dǎo)航控制進程)如算法3所示，其中modes變量的轉(zhuǎn)移關(guān)系如算法4所示，T_GPS_Reader線程模塊及其行為附件模塊如算法5所示。

算法3 導(dǎo)航控制進程模塊

算法4 modes變量的轉(zhuǎn)換關(guān)系

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

6.4 實驗案例——飛行控制系統(tǒng)的形式化驗證

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

6.4.1 安全屬性的驗證

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

1)可達性驗證

①Nav_Control_Process模塊modes的可達性驗證

如果當前模態(tài)為GPS_UP_AP_DOWN，驗證GPS_UP_AP_UP是否可達，該屬性對應(yīng)的CTL規(guī)范為

AG(modes=GPS_UP_AP_DOWN→

AF(modes=GPS_UP_AP_UP))

(17)

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

② T_GPS_Reader行為狀態(tài)的可達性驗證

T_GPS_Reader的行為附件的reader1狀態(tài)表示該線程調(diào)度完成，驗證reader1行為狀態(tài)是否可達。該屬性對應(yīng)的CTL規(guī)范為

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

(18)

驗證結(jié)果為TRUE表示T_GPS_Reader可以被正常調(diào)度，否則存在故障。

2)確定性驗證。

對Nav_Control_Process的GPS_DOWN模態(tài)進行確定性方面的驗證，模態(tài)的確定性保證了構(gòu)件不同的操作行為都可以正常執(zhí)行。該屬性對應(yīng)的CTL規(guī)范為

AF modes=GPS_DOWN

(19)

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

6.4.2 活性屬性的驗證

1) Nav_Control_Process的GPS_UP_AP_UP模態(tài)的活性驗證

GPS_UP_AP_UP表示GPS打開及自動導(dǎo)航打開模態(tài)，當人機交互子系統(tǒng)設(shè)置飛機為自動駕駛狀態(tài)時，導(dǎo)航控制進程會接收到自動導(dǎo)航指令，工作模態(tài)也會變成GPS_UP_AP_UP。該屬性對應(yīng)的CTL規(guī)范為

AG(AP_Toggle_event→AF(modes=

GPS_UP_AP_UP))

(20)

驗證結(jié)果為TRUE表示一旦飛行員設(shè)置飛機飛行狀態(tài)為自動駕駛，Nav_Control_Process進程會在GPS打開及自動導(dǎo)航打開(GPS_UP_AP_UP)模態(tài)下執(zhí)行。

2) T_GPS_Reader行為狀態(tài)的活性屬性驗證

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

AG(AP_Position_Input_event→AF(behavior_

specification.states=reader1))

(21)

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

6.4.3 模態(tài)配置的合法性驗證

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

當Nav_Control_Process以GPS_UP_AP_UP模態(tài)工作時，與自動導(dǎo)航計算線程T_AP_Compute線程有關(guān)的連接應(yīng)該是有效的。該屬性對應(yīng)的CTL規(guī)范為

A[!conn1.is Working U modes=

GPS_UP_AP_UP]

(22)

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

2) 子構(gòu)件模態(tài)配置的合法性驗證

T_AP_Compute僅在GPS_UP_AP_UP模態(tài)下才正常執(zhí)行。該屬性對應(yīng)的CTL規(guī)范為

AF(modes=GPS_UP_AP_UP &

T_AP_Compute.is Behavior)

(23)

驗證結(jié)果為TRUE表示T_AP_Compute符合Nav_Control_Process的模態(tài)配置定義，僅在GPS_UP_AP_UP模態(tài)下執(zhí)行，否則存在故障。

3) 流元素模態(tài)配置的合法性驗證

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

AG(modes=GPS_UP_AP_UP→AF(data=

Delta_Roll_Output))

(24)

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

4) 系統(tǒng)構(gòu)件下線程行為配置的合法性驗證Nav_Control_Process進程僅在自動飛行子系統(tǒng)模態(tài)為run時，才會正常執(zhí)行。而Nav_Control_Process內(nèi)的T_AP_Compute線程僅在進程模態(tài)為GPS_UP_AP_UP時，才會執(zhí)行。驗證系統(tǒng)模態(tài)為run模態(tài)時，T_AP_Compute線程是否會正常執(zhí)行。該屬性對應(yīng)的CTL規(guī)范為

AF (modes=run & Nav_Control_Process.

T_AP_Compute.is Behavior)

(25)

驗證結(jié)果為TRUE表示T_AP_Compute的行為符合系統(tǒng)模態(tài)的配置定義，否則存在故障。

6.5 驗證結(jié)果分析

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

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

1) 考慮的AADL子集更豐富，包括構(gòu)件、特征、連接、模態(tài)、數(shù)據(jù)流及行為附件等建模元素。

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

3) 對AADL模型中的安全性、活性、模態(tài)配置的正確性進行驗證，其中模態(tài)配置驗證包括連接子元素、子構(gòu)件及流元素的模態(tài)配置，以及系統(tǒng)層次化建模導(dǎo)致的模態(tài)嵌套正確性的驗證。

7 結(jié) 論

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

表2 實驗結(jié)果統(tǒng)計信息Table 2 Statistics of experimental results

表3 相關(guān)工作比較Table 3 Comparison of related works

續(xù)表3