李 蜜，莊 毅

(南京航空航天大學(xué) 計算機科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106)

0 引 言

隨著集成模塊化航電[1](IMA)概念的提出和廣泛應(yīng)用，使得嵌入式軟件的應(yīng)用日益普及，尤其是在航空航天等安全關(guān)鍵領(lǐng)域，不僅廣泛應(yīng)用了嵌入式軟件，更要求在應(yīng)用之前能夠?qū)η度胧杰浖目煽啃赃M行嚴格的驗證分析。AADL[2](architecture analysis and design language，體系結(jié)構(gòu)分析與設(shè)計語言)是于2004年由美國汽車工程師協(xié)會(society of automotive engineers，SAE)提出，并發(fā)布了與之對應(yīng)的SAE AS5506標準。自發(fā)布以來，AADL不斷完善，分別于2009年和2012年發(fā)布了經(jīng)過修訂的AS5506A標準和AS5506B標準。由于AADL本身所具有的巨大優(yōu)勢，得到了航空航天領(lǐng)域的支持，多所大學(xué)與研究機構(gòu)對AADL展開了深入研究與擴展[3-4]。這些研究涉及AADL標準擴展、建模工具、形式語義、可靠性分析等諸多方面，這些也是目前AADL的研究熱點。

AADL的建模形式是基于組件進行的，它支持兩種描述方式，分別是文本編輯和圖形化編輯，圖形化編輯方式可以建立直觀的模型。AADL通過附件(Annex)機制來擴展它的模型描述能力，從而提升可擴展性。附件需要經(jīng)過業(yè)界提議、發(fā)展以及核準才能成為AADL語言的一部分，已經(jīng)核準的附件有Graphical AADL Notation Annex，Error Model Annex以及UML Profile Annex等。其中Error Model Annex[5](EMA，錯誤模型附件)主要用于嵌入式軟件可靠性的建模[2,6-8],經(jīng)歷了兩個版本更新，EMV1(EMA volume1)和EMV2[9](EMA volume2)。

但是，AADL仍屬于一個半形式化的建模語言，也具有半形式化語言所固有的劣勢，不能很好地支持對軟件可靠性等非功能屬性的嚴格分析評估。需要為AADL添加形式化語義[10-14]，將其轉(zhuǎn)換為形式化模型，再對形式化模型進行嚴格驗證分析。

而Z語言[15]是一種基于一階邏輯謂詞與集合論的形式化規(guī)約語言，具有精確、簡潔、描述能力強等優(yōu)點，所建立的模型具有很好的可擴展性[16-17]，并且能夠采用現(xiàn)有的成熟工具對其進行類型檢查與確認。

而AADL與Z語言描述形式存在較大的區(qū)別，直接的模型轉(zhuǎn)換過程需要手動完善。為了實現(xiàn)AADL模型到Z語言模型的自動轉(zhuǎn)換，需要一種可以通過現(xiàn)有工具完成轉(zhuǎn)換的文檔結(jié)構(gòu)來描述AADL與Z語言[18]。XML(extensible markup language，擴展標記語言)是W3C的標準之一，提供了結(jié)構(gòu)化數(shù)據(jù)和文檔交換的通用格式。XMI(XML-based metadata interchange，基于XML的元模型轉(zhuǎn)換)是OMG組織提出的基于XML語言的元模型交換標準。XML文檔數(shù)據(jù)的轉(zhuǎn)換與顯示是通過添加文檔樣式信息來完成的，最常用的方法是基于XSLT來實現(xiàn)。XSL(extensible stylesheet language，擴展樣式表語言)在1999年由W3C提出，主要用于將一個XML文檔轉(zhuǎn)換為具有任意結(jié)構(gòu)的目標文檔，以及定義目標文檔的外觀。XSLT[19](extensible stylesheet language transformations，擴展樣式表轉(zhuǎn)換語言)是XSL的重要組成部分，定義了XML文檔的轉(zhuǎn)換語言。

文中首先研究了AADL與Z語言模型的轉(zhuǎn)換規(guī)則，然后通過AADL的建模工具OSATE(open source AADL tool environment)將AADL模型轉(zhuǎn)換到XML格式文檔，最后將基于XSLT的轉(zhuǎn)換工具集成到OSATE平臺上，完成AADL的XML格式文檔到Z語言模型文檔的自動轉(zhuǎn)換。

1 AADL到Z的轉(zhuǎn)換規(guī)則

1.1 AADL與Z

文中主要研究AADL可靠性模型到Z語言模型的轉(zhuǎn)換規(guī)則。AADL可靠性模型包括結(jié)構(gòu)模型與故障模型兩個部分，將兩者進行綁定可以描述軟件的故障行為，從而定義軟件的可靠性。圖1為AADL可靠性模型框架。

圖1 AADL可靠性模型框架

AADL組件分為三類：軟件組件、執(zhí)行平臺組件和系統(tǒng)組件。軟件組件包括線程(thread)，線程組(thread group)，進程(process)，數(shù)據(jù)(data)，子程序(subprogram group)；執(zhí)行平臺組件包括處理器(processer)，存儲器(memory)，設(shè)備(device)，總線(bus)；系統(tǒng)組件包括系統(tǒng)(system)與抽象(abstract)。AADL組件是由組件類型和組件實現(xiàn)共同定義的，組件類型明確類組件類別，定義了外部接口，以及可從外部查測的特性；組件實現(xiàn)則是對組件的內(nèi)部結(jié)構(gòu)進行說明，包括內(nèi)部隱含的屬性、包含的子組件等等。

在EMV1中故障模型與基本組件描述方法類似，由類型和實現(xiàn)兩部分組成。但在EMV2[9]中，故障模型則由故障類型、故障傳播、故障行為的方式分開說明。

Z語言的關(guān)鍵元素是類型系統(tǒng)與構(gòu)造單元。類型系統(tǒng)包括基本類型、冪集類型和枚舉類型等。構(gòu)造單元包括公理定義、模式(Schema)和通用式定義等。Schema是Z語言的基本結(jié)構(gòu)，包含聲明(Declaration)與謂詞(Predicate)兩部分，其中聲明部分用于聲明狀態(tài)空間或局部變量，而謂詞部分用于定義變量之間的約束。模式S通常采用如下的表示形式：

其中，v1,v2,…,vm為變量名，T1,T2,…,Tm分別為v1,v2,…,vm的類型，P1,P2,…,Pm為關(guān)于v1,v2,…,vm的約束。

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

AADL可靠性模型的轉(zhuǎn)換包括兩個部分：單個組件的轉(zhuǎn)換與組件間故障傳播的轉(zhuǎn)換。

AADL可靠性模型中每個故障模型與每個組件進行綁定，單個組件的轉(zhuǎn)換就是將組件的結(jié)構(gòu)、故障狀態(tài)、發(fā)生的故障行為等映射至Z語言模型對應(yīng)元素。其中故障行為可以通過故障事件以及事件引起的狀態(tài)轉(zhuǎn)移表示。

故障傳播則是指某組件發(fā)生故障時會影響與之有交互的組件。這種情況是模型轉(zhuǎn)換中的難點之一。

1.2.1 單個組件的轉(zhuǎn)換

以下是單個組件的轉(zhuǎn)換規(guī)則，因篇幅原因，部分模式僅以文字說明，未給出公式形式表達。

規(guī)則1：組件結(jié)構(gòu)轉(zhuǎn)換成Z語言的模式，模式聲明部分描述組件的端口、參數(shù)等結(jié)構(gòu)，謂詞部分可以給出結(jié)構(gòu)的約束，例如端口輸入或者輸出、參數(shù)的大小等等。

規(guī)則2：組件的故障類型通過Z語言的枚舉類型表示：[ErrorType]，ErrorType={ReplicationError, ServiceError,ValueRelatedError,TimingRelatedError…}。

規(guī)則3：組件的故障狀態(tài)通過Z語言的自定義類型表示：[ErrorState]，每個組件的故障狀態(tài)不一定相同，因此不同組件故障狀態(tài)映射的ErrorType會有所不同。

規(guī)則4：組件的故障事件(ErrorEvent，Ee)轉(zhuǎn)換成Z語言的模式，模式聲明部分描述故障事件發(fā)生的概率分布，謂詞部分則是給出概率分布的相關(guān)約束。其中概率的分布類型通過枚舉類型表示：[DistributionType]，DistributionType={Fixed,Poisson,Normal,Gauss,Weibull…}。模式的垂直形式如下：

在該模式中，<>中的元素為可替換項，Occurrence表示概率，Distribution表示概率的分布類型，R表示實數(shù)，0..1表示處于0至1之間(包含邊界)。

規(guī)則5：組件的狀態(tài)轉(zhuǎn)移轉(zhuǎn)換成Z語言的模式，模式聲明部分描述導(dǎo)致狀態(tài)轉(zhuǎn)移的轉(zhuǎn)移動作，以及轉(zhuǎn)移的前后狀態(tài)，謂詞部分給出狀態(tài)轉(zhuǎn)移需要滿足的必要條件。模式垂直形式如下：

1.2.2 故障傳播的轉(zhuǎn)換

AADL可靠性模型中的故障傳播包括故障傳播點(ErrorPropagationPoint，Epp)、故障傳播的路徑。故障傳播點包括傳入故障點incoming、傳出故障點outgoing。而故障傳播路徑在AADL中用流(Flow)表示，流定義了組件從輸入到輸出的邏輯流，可以描述組件之間數(shù)據(jù)流、控制流或者故障流。

以下為故障傳播的轉(zhuǎn)換規(guī)則。

規(guī)則1：故障傳播點轉(zhuǎn)換成Z語言的模式，聲明部分描述故障傳播點的類型。而故障傳播點的類型通過枚舉類型表示：[EppType]，EppType={incoming,outgoing}。

規(guī)則2：故障傳播路徑轉(zhuǎn)換成Z語言的模式，模式聲明部分描述故障傳播經(jīng)過的傳播點，用以表示傳播路徑，謂詞部分給出相關(guān)約束。模式的垂直形式如下：

在該模式中，Epp即規(guī)則1所轉(zhuǎn)換得到的模式。

2 基于XSLT的自動模型轉(zhuǎn)換

OSATE是由卡耐基梅隆大學(xué)開發(fā)的一款開源AADL建模環(huán)境。OSATE以eclipse插件形式提供了AADL的建模、驗證與分析工具。建模工具支持AADL文本、圖形和XML三種視圖的同步建立、更新與轉(zhuǎn)換。

在完成AADL可靠性模型的建模與對應(yīng)XML源文檔的生成后，需要根據(jù)轉(zhuǎn)換規(guī)則設(shè)計XSLT樣式表。根據(jù)第1節(jié)提出的轉(zhuǎn)換規(guī)則，描述一個完整的AADL可靠性模型需要以下元素：組件結(jié)構(gòu)模式、故障事件模式、狀態(tài)轉(zhuǎn)移模式、故障傳播點模式、故障傳播路徑模式和一些數(shù)據(jù)類型。所以在轉(zhuǎn)換過程中要分階段對源文檔進行遞歸處理。另外，在設(shè)計過程中會用到Z模式中一些特有的標識符，所以在設(shè)計之前需要在實驗環(huán)境中增加相應(yīng)的Z語言字符集。

XSLT樣式表部分內(nèi)容如圖2所示。

圖2 XSLT樣式表實例

圖2中樣式表的┌與└符號表示輸出模式的標識符，會直接輸出。其次，用元素輸出模式的模式名，命名格式為“[name]+Event”，name與XML源文檔中對應(yīng)元素相同，Event可以不加。樣式表中的“|”則對應(yīng)Z語言模式中的分隔線，將聲明與謂詞部分分隔。

以上是以故障事件為例簡單說明了XSLT的設(shè)計過程，由于XSLT語言的模塊化特性，可通過添加模式表模板來匹配更多AADL元素，從而實現(xiàn)AADL模型的自動轉(zhuǎn)換。

總結(jié)基于XSLT的轉(zhuǎn)換過程如下：在OSATE平臺上建立AADL的可靠性模型，并轉(zhuǎn)換為XML格式的源文檔。根據(jù)建立的AADL到Z的轉(zhuǎn)換規(guī)則設(shè)計XSLT樣式表，將AADL可靠性模型進行轉(zhuǎn)換，最后輸出目標文檔，得到Z語言模型。圖3展示了AADL到Z的轉(zhuǎn)換流程。

圖3 AADL到Z的轉(zhuǎn)換流程

3 實例研究

文獻[2]中以一個飛行控制系統(tǒng)作為示例描述了AADL可靠性的建模過程。文中對該系統(tǒng)的自動駕駛子系統(tǒng)的功能需求進行細化，以此作為示例對文中模型轉(zhuǎn)換方法進行應(yīng)用說明。

3.1 實例描述

圖4是自動駕駛子系統(tǒng)的AADL架構(gòu)，包含4個作動器(Aileron、Elevator、Rudder與Engine)與1個GPS傳感器。作動器用來控制飛行器的飛行狀態(tài)，GPS用來獲取當(dāng)前定位信息。還包括了計算線程(AP_Computer)、讀取GPS數(shù)據(jù)線程(GPS_Reader)、參數(shù)設(shè)置線程(AP_Params)等四個線程組件。該子系統(tǒng)的功能是通過4個作動器和GPS傳感器的交互來控制飛行控制系統(tǒng)狀態(tài)。文中以設(shè)備GPS與線程GPS_Reader為例說明模型轉(zhuǎn)換方法。

圖4 自動駕駛子系統(tǒng)AADL架構(gòu)

3.2 自動轉(zhuǎn)換過程

GPS的AADL可靠性模型如圖5所示，主要包含兩個部分：故障行為與GPS組件的類型及實現(xiàn)。故障行為中描述了一個故障事件CatchFail、兩個故障狀態(tài)Error_Free和Failed、一個狀態(tài)轉(zhuǎn)移BadValue Transition，并在屬性中給出了故障事件的概率分布，概率為0.003，分布類型為定值Fixed。在GPS組件的類型中描述了兩個端口send1與send2，send1為輸出數(shù)據(jù)端口，send2為輸出事件端口。GPS組件類型中還包含了一個annex EMV2，在其中描述了組件采用的故障模型庫、故障行為、故障傳播點(用send1、send2表示)與故障傳播流(GtoR)。

圖5 GPS的AADL可靠性模型

GPS_Reader的AADL可靠性模型與GPS類似。

圖6是GPS的AADL可靠性模型對應(yīng)的XML源文檔。從圖中可以看到GPS的故障行為CFT被轉(zhuǎn)換為XML文檔中的樹狀結(jié)構(gòu)。

圖6 GPS的AADL可靠性模型XML源文檔

轉(zhuǎn)換規(guī)則對應(yīng)的XSLT樣式表設(shè)計過程按第2節(jié)所述方法進行。最后通過基于XSLT樣式表轉(zhuǎn)換得到的目標Z語言模型文檔(部分)如圖7所示。其中GtoR表示故障傳播流，send1是GPS組件的故障傳出點、recv是GPS_Reader的故障傳入點，在謂詞約束中對傳入傳出類型進行約束。

圖7 Z語言模型文檔

將圖7所示的部分轉(zhuǎn)換結(jié)果與圖5所示的部分AADL進行對比，可以看出，圖7的Z模型中描述的CatchFail、send1和GtoR均在圖5的AADL中有定義，并且在轉(zhuǎn)換過程中，這些組件的可靠性約束完整、無丟失。比如，send1在AADL先被定義為out data port類型，即為數(shù)據(jù)輸出接口，后在定義flows類型的GtoR時又被定義為故障源接口，即為故障輸傳出點；在圖7的send1模式中，將send1直接定義為了故障傳出點，符合轉(zhuǎn)換要求。這驗證了文中轉(zhuǎn)換方法的正確性和有效性。

4 結(jié)束語

針對AADL難以嚴格驗證評估軟件可靠性的問題，在對AADL與Z語言語法語義研究的基礎(chǔ)上，提出AADL到Z的轉(zhuǎn)換規(guī)則，分別研究了單個組件以及組件間故障傳播的轉(zhuǎn)換規(guī)則。并基于XSLT實現(xiàn)了AADL到Z的自動轉(zhuǎn)換方法，從實例研究中可以看到，該方法可以將AADL中的相關(guān)元素都轉(zhuǎn)換到Z語言模型中。基于文中的研究工作，可以在軟件開發(fā)的設(shè)計階段建立直觀的AADL可靠性模型，而通過AADL到Z的轉(zhuǎn)換有助于后續(xù)的可靠性評估工作。