程亦涵，黃志球，闞雙龍

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

1 引言

隨著嵌入式軟件不斷發(fā)展，軟件開(kāi)發(fā)規(guī)模逐漸擴(kuò)大，軟件復(fù)雜度不斷增加，以及其在汽車(chē)、核能、航空、航天等安全關(guān)鍵領(lǐng)域的廣泛應(yīng)用，使人們對(duì)嵌入式軟件的可靠性和安全性有更高的要求。軟件失效所引起的安全事故頻發(fā)，使保障嵌入式軟件的安全性成為近年來(lái)軟件工程領(lǐng)域的研究熱點(diǎn)。為了解決上述問(wèn)題，出現(xiàn)很多新的方法，其中最突出的就是模型驅(qū)動(dòng)開(kāi)發(fā)MDD（Model Driven Development）［1］。

模型驅(qū)動(dòng)開(kāi)發(fā)是一種以模型為主體的高級(jí)別抽象開(kāi)發(fā)方法。模型驅(qū)動(dòng)開(kāi)發(fā)能為各個(gè)開(kāi)發(fā)階段提供全局統(tǒng)一的視圖和指導(dǎo)，能在開(kāi)發(fā)早期對(duì)模型進(jìn)行驗(yàn)證，盡早發(fā)現(xiàn)錯(cuò)誤。常用的MDD 模型有UML、SysML等。

2004年11月，汽車(chē)工程師協(xié)會(huì)SAE（Society of Automotive Engineers）發(fā) 布 了 航 空 標(biāo) 準(zhǔn)AS5506，命 名 為AADL（Architecture Analysis and Design Language）［2，3］。AADL是一種應(yīng)用于嵌入式系統(tǒng)領(lǐng)域的體系結(jié)構(gòu)建模語(yǔ)言，支持航空、航天、汽車(chē)等領(lǐng)域復(fù)雜實(shí)時(shí)的安全關(guān)鍵系統(tǒng)的設(shè)計(jì)與分析。AADL提供了標(biāo)準(zhǔn)化的文本和圖形符號(hào)以描述軟件、硬件系統(tǒng)架構(gòu)以及其功能接口。同時(shí)，AADL支持各種類(lèi)型的分析，以保障其行為和建模系統(tǒng)性能符合需求。

當(dāng)定義的初始屬性不能滿(mǎn)足用戶(hù)需要時(shí)，AADL 引入了附件的概念。附件擁有獨(dú)立的語(yǔ)法和語(yǔ)義，但必須與AADL核心語(yǔ)義標(biāo)準(zhǔn)保持一致。SAE在2006年發(fā)布的AS5506/1標(biāo)準(zhǔn)中提出了錯(cuò)誤模型附件（Error Model Annex）［4］，附件通過(guò)定義一組聲明和語(yǔ)義指明AADL體系結(jié)構(gòu)中組件和連接的錯(cuò)誤模型。通過(guò)錯(cuò)誤模型附件，我們可以對(duì)一個(gè)AADL體系結(jié)構(gòu)模型的系統(tǒng)屬性，如安全性、可靠性、完整性等，進(jìn)行定性和定量評(píng)估。

AADL本身是一個(gè)具有確定語(yǔ)義定義并且有嚴(yán)格語(yǔ)法的半形式化建模語(yǔ)言，要對(duì)AADL 系統(tǒng)架構(gòu)模型進(jìn)行相應(yīng)的非功能屬性分析，還需要對(duì)AADL系統(tǒng)架構(gòu)模型中的構(gòu)件屬性進(jìn)行形式化描述，然后再借用形式化理論方法和相關(guān)工具來(lái)驗(yàn)證系統(tǒng)模型的非功能屬性是否滿(mǎn)足需求。AADL 錯(cuò)誤模型附件中提到，含有錯(cuò)誤模型的AADL 體系結(jié)構(gòu)模型可以支持多種方式的分析，如故障樹(shù)可以從規(guī)范出發(fā)分析其安全性，馬爾科夫鏈分析法可以用于評(píng)估其可信性和可用性，但馬爾科夫鏈模型無(wú)法對(duì)系統(tǒng)構(gòu)件間的交互行為進(jìn)行動(dòng)態(tài)的描述。為了對(duì)系統(tǒng)構(gòu)件間的交互行為進(jìn)行動(dòng)態(tài)的描述，往往需要采用更高級(jí)的形式化語(yǔ)言，如廣義隨機(jī)Petri網(wǎng)GSPNs（Generalized Stochastic Petri Nets）［5］。本文采用交互式馬爾科夫鏈IMC（Interactive Markov Chains）［6］對(duì)AADL 模型中構(gòu)件及其錯(cuò)誤狀態(tài)可能的失效進(jìn)行刻畫(huà)，建立IMC 可靠性計(jì)算模型，通過(guò)分析得出原AADL 模型是否滿(mǎn)足設(shè)計(jì)要求。

本文第2節(jié)結(jié)合已有工作介紹AADL模型分析的相關(guān)問(wèn)題和研究；第3節(jié)介紹AADL 可靠性模型及其建立方法；第4節(jié)介紹IMC 的交互動(dòng)作語(yǔ)義，并給出從AADL可靠性模型到IMC 模型的轉(zhuǎn)化規(guī)則；第5節(jié)結(jié)合法國(guó)空中交通控制系統(tǒng)的實(shí)例，通過(guò)第4節(jié)的規(guī)則，轉(zhuǎn)化得到相應(yīng)的IMC模型進(jìn)行定量分析，得到結(jié)果反饋給原模型；第6節(jié)為總結(jié)與展望。

2 相關(guān)工作

隨著模型驅(qū)動(dòng)開(kāi)發(fā)在工業(yè)界廣泛應(yīng)用，很多組織開(kāi)始基于AADL 模型進(jìn)行設(shè)計(jì)與分析研究，并開(kāi)發(fā)了一系列相關(guān)設(shè)計(jì)分析工具。其中，卡內(nèi)基梅隆大學(xué)軟件工程研究所SEI（Software Engineering Institute）基于Eclipse平臺(tái)開(kāi)發(fā)了開(kāi)源AADL 設(shè)計(jì) 工 具OSATE［7］。OSATE 提 供 從 前 到 后 對(duì)AADL模型進(jìn)行處理的工具集，可以以XML 文本文件或圖形的方式表示AADL 模型文件，并對(duì)AADL模型文件進(jìn)行語(yǔ)法和語(yǔ)義的檢查。由于OSATE是開(kāi)源的，為其他的基于AADL 模型的分析提供了環(huán)境。許多研究者以O(shè)SATE 環(huán)境為基礎(chǔ)研究開(kāi)發(fā)針對(duì)AADL 模型屬性分析的工具，如AADL模型仿真測(cè)試工具AADS［8］。類(lèi)似的建模工具還有STOOD。

在AADL模型可靠性分析方面，Rugina A 在2006年提出AADL 可靠性模型（AADL Dependability Model）。結(jié)合AADL 可靠性模型，Rugina A 在文獻(xiàn)［5］提出了一種AADL 分析方法，將AADL可靠性模型轉(zhuǎn)化為GSPN，進(jìn)行形式化分析驗(yàn)證，并設(shè)計(jì)實(shí)現(xiàn)了相關(guān)工具ADATP。文獻(xiàn)［9］基于Rugina A 的研究，設(shè)計(jì)了一套完整的工具集對(duì)AADL模型進(jìn)行定性和定量分析。

在AADL模型可靠性方面，國(guó)內(nèi)也有相關(guān)研究，文獻(xiàn)［10］提出了一種AADL 向馬爾科夫鏈轉(zhuǎn)化的方法，并結(jié)合需求，分析模型是否符合要求。文獻(xiàn)［11］和文獻(xiàn)［12］將AADL 與UPPAAL 驗(yàn)證工具結(jié)合，分別驗(yàn)證了AADL 模型的可調(diào)度性和行為模型的正確性。文獻(xiàn)［13］和文獻(xiàn)［14］將AADL可靠性模型轉(zhuǎn)化到GSPN，并設(shè)計(jì)實(shí)現(xiàn)了AADL模型可靠性分析評(píng)估工具ARAM。

AS5506/1標(biāo)準(zhǔn)中提到：馬爾科夫分析方法可以定量分析錯(cuò)誤模型的可信性和可用性。但是，馬爾科夫鏈在描述復(fù)雜系統(tǒng)時(shí)有自身的局限性：無(wú)法描述系統(tǒng)構(gòu)件之間的交互動(dòng)作。故上文提到的工作大都將AADL 可靠性模型轉(zhuǎn)化到GSPN，再通過(guò)GSPN 內(nèi)部的分析方法進(jìn)行定量分析，但GSPN在分析可靠性的時(shí)候，仍然需要轉(zhuǎn)化到馬科夫鏈，進(jìn)行馬爾科夫鏈分析。本文提出一種模型轉(zhuǎn)化方法，將AADL可靠性模型轉(zhuǎn)化到交互式馬爾科夫鏈。由于交互式馬爾科夫鏈?zhǔn)且环N功能行為和性能指標(biāo)混合的并發(fā)系統(tǒng)模型，所以它既可以直接進(jìn)行馬爾科夫分析，又可以對(duì)模型進(jìn)行定性分析，為AADL可靠性模型研究提供一種新的思路。

3 AADL可靠性模型研究

AADL可靠性模型由AADL系統(tǒng)架構(gòu)模型和AADL錯(cuò)誤模型組成。系統(tǒng)架構(gòu)模型從軟件、硬件兩方面描述系統(tǒng)架構(gòu)，描述了系統(tǒng)內(nèi)部組件之間的連接以及相互依賴(lài)關(guān)系；AADL 錯(cuò)誤模型附件定義了構(gòu)件和連接建立故障模型的聲明規(guī)則和語(yǔ)義。AADL系統(tǒng)架構(gòu)模型通過(guò)類(lèi)型（Type）和實(shí)現(xiàn)（Implementation）兩部分定義整體模型。類(lèi)型定義了模型的外部可見(jiàn)特性，如接口、屬性等；實(shí)現(xiàn)定義了模型的內(nèi)部特性，如交互、子組件等。與AADL系統(tǒng)架構(gòu)模型一樣，AADL 錯(cuò)誤模型也是由兩部分組成：（1）錯(cuò)誤類(lèi)型（Error Model Type）定義了錯(cuò)誤模型的基本要素：錯(cuò)誤狀態(tài)、事件等；（2）錯(cuò)誤實(shí)現(xiàn)定義了由錯(cuò)誤事件和錯(cuò)誤傳播引起的錯(cuò)誤狀態(tài)之間的變遷。

AADL體系結(jié)構(gòu)模型可以提供組件之間的依賴(lài)關(guān)系以及與可靠性相關(guān)的信息，如故障、失效模式、修復(fù)機(jī)制、錯(cuò)誤傳播路徑等等，結(jié)合錯(cuò)誤模型附件的基本錯(cuò)誤附錄庫(kù)，可以得出相應(yīng)的可靠性模型。

錯(cuò)誤類(lèi)型聲明一組錯(cuò)誤狀態(tài)（Error State）、錯(cuò)誤事件（Error Event）以及錯(cuò)誤傳播（Error Propagations）。發(fā)生（Occurrence）屬性表示到達(dá)率或者事件或傳播發(fā)生的概率。錯(cuò)誤模型實(shí)現(xiàn)聲明了錯(cuò)誤狀態(tài)之間的轉(zhuǎn)化（Error Transitions）。圖1是一個(gè)簡(jiǎn)單的沒(méi)有錯(cuò)誤傳播的錯(cuò)誤模型范例。如圖1所示，初始狀態(tài)是無(wú)錯(cuò)誤狀態(tài)，錯(cuò)誤狀態(tài)有Erroneous和Failed 兩個(gè)，分別對(duì)應(yīng)Temp＿Fault和Perm＿Fault兩個(gè)錯(cuò)誤事件，而Restart和Recover則是系統(tǒng)自行修復(fù)的事件。

Figure 1 An error model example without propagations圖1 簡(jiǎn)單錯(cuò)誤模型

AADL體系結(jié)構(gòu)模型中，不同組件之間存在交互，而組件的錯(cuò)誤模型也存在交互。錯(cuò)誤模型的交互由組件之間的連接和依賴(lài)關(guān)系確定。AS5506/1標(biāo)準(zhǔn)將錯(cuò)誤傳播分為Out－propagation和In－propagation 兩 種。Out－propagation 通 過(guò) 組件之間的連接和依賴(lài)關(guān)系將錯(cuò)誤傳播給其他組件；而In－propagation只會(huì)接受相應(yīng)的組件傳播過(guò)來(lái)的錯(cuò)誤。一個(gè)Out－propagation 可能會(huì)對(duì)應(yīng)多個(gè)In－propagation。此時(shí)，必須通過(guò)組件之間的依賴(lài)關(guān)系 來(lái) 確 定Out－propagation 所 對(duì) 應(yīng) 的In－propagation。圖2中，圖2a表示在AADL模型中組件1與組件2之間有數(shù)據(jù)連接；圖2b表示組件2對(duì)組件1有依賴(lài)；圖2c表示當(dāng)錯(cuò)誤發(fā)生，錯(cuò)誤模型中，組件1與組件2之間的依賴(lài)關(guān)系。由此，我們可以得出對(duì)應(yīng)的帶依賴(lài)關(guān)系的錯(cuò)誤模型，并對(duì)其進(jìn)行模型轉(zhuǎn)化，得到相應(yīng)形式化模型進(jìn)行驗(yàn)證。

Figure 2 Architecture－based dependency圖2 組件之間的依賴(lài)關(guān)系

圖3是組件1對(duì)應(yīng)的錯(cuò)誤模型，從圖3中我們可以看到，在錯(cuò)誤模型類(lèi)型中，定義了out error propagation屬性，表示錯(cuò)誤傳播，系統(tǒng)需要判斷該錯(cuò)誤是否發(fā)生傳播，其發(fā)生的概率是固定概率p，而在錯(cuò)誤實(shí)現(xiàn)中，定義了錯(cuò)誤轉(zhuǎn)移發(fā)送的信息Erroneous。組件2 的錯(cuò)誤模型定義沒(méi)有在這里提出，它與1唯一的不同是在接收錯(cuò)誤的時(shí)候，當(dāng)2接受到組件1發(fā)送的錯(cuò)誤時(shí)，會(huì)從Error＿free狀態(tài)轉(zhuǎn)換到Failed。

Figure 3 An error model example with dependency圖3 帶有依賴(lài)關(guān)系的錯(cuò)誤模型

在錯(cuò)誤模型建立時(shí)，我們需要考慮組件之間的相互依賴(lài)關(guān)系，同時(shí)，我們還需要考慮錯(cuò)誤模型與系統(tǒng)模型之間的連接，因?yàn)殄e(cuò)誤發(fā)生之后，會(huì)對(duì)系統(tǒng)產(chǎn)生影響（如備用系統(tǒng)的啟用等）。在AADL中，通常使用Guard＿Transition屬性來(lái)連接。

圖4所示為錯(cuò)誤模型中發(fā)生的錯(cuò)誤對(duì)系統(tǒng)模型產(chǎn)生的影響，其中，g1～g6 行為系統(tǒng)模型通過(guò)Guard＿Transition 屬性與錯(cuò)誤模型相關(guān)聯(lián)。當(dāng)Comp1 處 于FailedVisible狀 態(tài)、Comp2 處 于Error＿Free狀態(tài)時(shí)（g1～g3），系統(tǒng)應(yīng)執(zhí)行Comp1.Send2和Comp2.Send1，使系統(tǒng)切換到備用組件，反之則應(yīng)切換回主組件。通過(guò)Guard＿Transition屬性，錯(cuò)誤組件與系統(tǒng)組件相關(guān)聯(lián)，使其能更好地反映錯(cuò)誤事件發(fā)生對(duì)整個(gè)系統(tǒng)造成的影響。

當(dāng)我們得出帶有依賴(lài)關(guān)系的錯(cuò)誤模型后，就可以將完整的可靠性模型轉(zhuǎn)化到形式化模型進(jìn)行驗(yàn)證分析。

Figure 4 Guard＿Transition property associations in the AADL model圖4 AADL模型中的Guard＿Transition屬性

4 IMC模型以及轉(zhuǎn)換規(guī)則

4.1 IMC模型

IMC模型作為一種可以組合化的性能評(píng)價(jià)模型由德國(guó)學(xué)著Hermanns H 于1998年提出，其最大的優(yōu)點(diǎn)是在刻畫(huà)系統(tǒng)性能特征的同時(shí)還提供了對(duì)復(fù)雜并發(fā)系統(tǒng)的組合描述能力，使得對(duì)復(fù)雜并發(fā)系統(tǒng)的性能評(píng)價(jià)可以得到簡(jiǎn)化。IMC 模型與其他基于動(dòng)作的并發(fā)系統(tǒng)模型有很大不同，它結(jié)合了系統(tǒng)的性能特征，同時(shí)又是一個(gè)交織語(yǔ)義的模型。IMC模型實(shí)際上是標(biāo)記轉(zhuǎn)移系統(tǒng)LTS（Labeled Transition System）和帶標(biāo)記的連續(xù)時(shí)間馬爾科夫鏈 labeled CTMC （labeled Continuous－Time Markov Chains）這兩個(gè)系統(tǒng)的綜合。

一個(gè)IMC是一個(gè)五元組（S，Act，→ ，?，s0），其中

（1）S是一個(gè)非空狀態(tài)集合。

（2）Act是一個(gè)動(dòng)作集合。

（3）→S×Act×S是一個(gè)動(dòng)作轉(zhuǎn)移關(guān)系，通常將（s，a，s′）∈→記 作

其中，R為轉(zhuǎn)移率矩陣。

（5）S0是初始狀態(tài)。

定義中的兩個(gè)轉(zhuǎn)移關(guān)系分別是LTS中的動(dòng)作轉(zhuǎn)移與CTMC中的馬爾科夫轉(zhuǎn)移，其含義基本保持不變。（4）中的λ表示轉(zhuǎn)移率，與轉(zhuǎn)移概率不同，轉(zhuǎn)移率λ與時(shí)間長(zhǎng)短是無(wú)關(guān)的。這些轉(zhuǎn)移率構(gòu)成一個(gè)轉(zhuǎn)移率矩陣R。由上述定義可以看出，IMC在定義中將LTS與CTMC 的各部分元素基本上是沒(méi)有改變地結(jié)合在一起，這樣就最大可能地保持了LTS和CTMC 兩個(gè)系統(tǒng)原有的性質(zhì)。圖5 是一個(gè)簡(jiǎn)單的IMC圖示。

Figure 5 An example of interactive Markov chains圖5 交互式馬爾科夫鏈圖示

兩種系統(tǒng)的結(jié)合，使得IMC 可以更加全面地描述一個(gè)復(fù)雜嵌入式系統(tǒng)，特別是描述并行系統(tǒng)。圖6中P和Q是兩個(gè)簡(jiǎn)單的操作：（1）P從s0開(kāi)始，經(jīng)過(guò)參數(shù)為λ馬爾科夫轉(zhuǎn)移到達(dá)狀態(tài)s1，再執(zhí)行動(dòng)作a到達(dá)s2；（2）Q與P類(lèi)似，也需要執(zhí)行動(dòng)作a，到達(dá)最終狀態(tài)。當(dāng)P與Q并行執(zhí)行的時(shí)候，即圖6所示的P‖aQ，IMC 完美地解決了并行執(zhí)行的問(wèn)題。

Figure 6 Icon of IMC parallel execution圖6 IMC并行執(zhí)行圖示

4.2 轉(zhuǎn)化規(guī)則

本文選用IMC 模型作為系統(tǒng)可靠性計(jì)算模型，并建立AADL可靠性模型與IMC 模型之間的對(duì)應(yīng)轉(zhuǎn)化關(guān)系。主要通過(guò)以下兩步來(lái)完成：（1）基本元素之間的對(duì)應(yīng)轉(zhuǎn)化；（2）相關(guān)組件之間的inout propagation轉(zhuǎn)化到對(duì)應(yīng)IMC模型。

4.2.1 基本元素對(duì)應(yīng)轉(zhuǎn)化

AADL模型與IMC模型之間基本元素的轉(zhuǎn)化是比較簡(jiǎn)單的，因?yàn)锳ADL 錯(cuò)誤模型通常表示成一個(gè)隨機(jī)自動(dòng)機(jī)，一個(gè)組件只作為一個(gè)狀態(tài)。表1是基本元素之間的轉(zhuǎn)化規(guī)則。

Table 1 Basic AADL error model to IMC transformation rules表1 AADL模型基本元素與IMC的對(duì)應(yīng)轉(zhuǎn)化

有了上述基本元素轉(zhuǎn)化關(guān)系，我們可以將之前圖1中提到的簡(jiǎn)單的錯(cuò)誤模型轉(zhuǎn)化到IMC 模型，具體如圖7所示。

Figure 7 Corresponding IMC model to the error model in figure 1圖7 圖1所示簡(jiǎn)單錯(cuò)誤模型對(duì)應(yīng)的IMC模型

4.2.2 In－out propagation 轉(zhuǎn)換規(guī)則

前文中我們提到，Error Model Annex中定義了AADL模型中的錯(cuò)誤傳播，用In－out propagation來(lái)表示。Out－propagation表示錯(cuò)誤向組件外傳播，并到達(dá)指定接收組件即In－propagation。一個(gè)Out－propagation可以對(duì)應(yīng)多個(gè)In－propagation，通過(guò)組件之間的依賴(lài)關(guān)系，我們可以得出相應(yīng)的帶依賴(lài)關(guān)系的錯(cuò)誤模型（如圖3所示），根據(jù)名稱(chēng)匹配找到與Out－propagation相對(duì)應(yīng)的In－propagation。如圖8 所示，組件1 作為發(fā)送者，向外傳播名為Error的錯(cuò)誤，而組件2作為接收者接收一個(gè)錯(cuò)誤傳播，名為Error。這樣兩個(gè)組件為一對(duì)In－out propagation。

在定義In－out propagation轉(zhuǎn)化規(guī)則的時(shí)候，首先要將Out與In區(qū)分開(kāi)。因?yàn)槿绻鸒ut－propagation發(fā)生，則接收組件一定能接收到傳播過(guò)來(lái)的錯(cuò)誤信息。圖9 是帶有傳播的錯(cuò)誤模型轉(zhuǎn)化到IMC模型的范例。Sender發(fā)生錯(cuò)誤后，有一定概率將這個(gè)錯(cuò)誤傳播出去，根據(jù)依賴(lài)關(guān)系，該錯(cuò)誤信息將發(fā)送給Receiver，收到錯(cuò)誤信息之后，Receiver從Error＿Free狀態(tài)轉(zhuǎn)換到Failed狀態(tài)。

5 實(shí)例分析

本文將結(jié)合法國(guó)空中交通控制系統(tǒng)，先建立AADL可靠性模型，再通過(guò)上述模型轉(zhuǎn)換規(guī)則得到IMC模型，并對(duì)其進(jìn)行可靠性分析，通過(guò)結(jié)果對(duì)原系統(tǒng)兩種備選方案選擇提出參考。

Figure 8 Sender and receiver—name matching propagations圖8 錯(cuò)誤傳播中的名稱(chēng)匹配

Figure 9 IMC model with propagations圖9 帶有傳播的IMC模型

5.1 系統(tǒng)AADL模型

如圖10所示，該系統(tǒng)是由兩個(gè)分布式軟件組件集合組成：飛行計(jì)劃（flight plans，F(xiàn)Punit）和雷達(dá)數(shù)據(jù)（radar data，RDunit）。建立體系結(jié)構(gòu)模型有a、b兩種方案。FPunit與RDunit內(nèi)部結(jié)構(gòu)相同：都擁有兩個(gè)線(xiàn)程Comp1（主要）和Comp2（備用），這是為了提高系統(tǒng)的可靠性和安全性，在設(shè)計(jì)FPunit和RDunit構(gòu)件時(shí)加入了冗余構(gòu)件，即這兩個(gè)構(gòu)件存在備用線(xiàn)程（Comp2），在主要線(xiàn)程（Comp1）出現(xiàn)故障時(shí)會(huì)自動(dòng)切換到備用構(gòu)件繼續(xù)完成功能。a 和b 兩個(gè)方案都使用兩個(gè)處理器（processor1和processor2）。

a和b的區(qū)別在于：方案a中，RD＿Comp1 和FP＿Comp1分別由不同的處理器處理（RD＿Comp1與Processor2 綁 定，F(xiàn)P＿Comp1 與Processor1 綁定）；而方案b中，RD＿Comp1 和FP＿Comp1 綁定同一個(gè)處理器。整個(gè)系統(tǒng)有兩個(gè)操作狀態(tài)：正常和重配置。兩個(gè)處理器通過(guò)總線(xiàn)相連。當(dāng)總線(xiàn)出現(xiàn)錯(cuò)誤時(shí)，會(huì)導(dǎo)致RDunit出現(xiàn)故障從而導(dǎo)致系統(tǒng)失效，而RDunit會(huì)從FPunit接收錯(cuò)誤傳播。

5.2 依賴(lài)關(guān)系分析及錯(cuò)誤模型的建立

組件之間的依賴(lài)關(guān)系主要來(lái)源于它們之間的交互，根據(jù)上面的體系結(jié)構(gòu)圖，可以得出如下依賴(lài)關(guān)系：

（1）處理器與其運(yùn)行的線(xiàn)程之間有結(jié)構(gòu)依賴(lài)關(guān)系。圖10a中的S1、S2、S3和S4反映這種依賴(lài)關(guān)系。

（2）同時(shí)，處理器與其運(yùn)行的線(xiàn)程還有恢復(fù)依賴(lài)關(guān)系。如果一個(gè)線(xiàn)程出錯(cuò)，則正在運(yùn)行錯(cuò)誤狀態(tài)的處理器不能重啟。圖10a中的R1、R2、R3和R4反映這種依賴(lài)關(guān)系。

Figure 10 Two candidate AADL architecture models of the air traffic control system圖10 空中交通控制系統(tǒng)的兩個(gè)備選AADL體系結(jié)構(gòu)模型

（3）兩個(gè)處理器之間還有維護(hù)依賴(lài)性，但圖10中并未體現(xiàn)這一點(diǎn)。

（4）圖10 中 的FT1 和FT2 反 映 了 兩 個(gè) 線(xiàn) 程之間的錯(cuò)誤容忍依賴(lài)：當(dāng)一個(gè)線(xiàn)程出現(xiàn)錯(cuò)誤，可以切換到另一個(gè)正常線(xiàn)程，保證系統(tǒng)繼續(xù)運(yùn)行。

（5）圖10b中F3反映了總線(xiàn)和線(xiàn)程之間的結(jié)構(gòu)依賴(lài)。當(dāng)總線(xiàn)出錯(cuò)，會(huì)斷開(kāi)與線(xiàn)程之間的連接，使其可以從正常狀態(tài)切換到重配置狀態(tài)，完成相應(yīng)的功能。

（6）FPunit與RDunit之間有功能依賴(lài)關(guān)系，F(xiàn)Punit出現(xiàn)錯(cuò)誤之后可能會(huì)將錯(cuò)誤傳播給RDunit，圖10中的F1和F2反映這個(gè)依賴(lài)關(guān)系。相反，RDunit出現(xiàn)錯(cuò)誤卻不會(huì)傳播給FPunit，這在建立錯(cuò)誤模型時(shí)尤為關(guān)鍵。

根據(jù)上述依賴(lài)關(guān)系，我們可以建立對(duì)應(yīng)錯(cuò)誤模型。為了簡(jiǎn)化整個(gè)模型，我們重點(diǎn)關(guān)注FPunit和RDunit之間的依賴(lài)關(guān)系，不考慮處理器內(nèi)部的情況。圖11為FPunit線(xiàn)程的錯(cuò)誤模型，f1、f2對(duì)應(yīng)FPunit和RDunit之間的功能依賴(lài)關(guān)系（圖10 中的F1和F2），t1～t4對(duì)應(yīng)線(xiàn)程中的錯(cuò)誤容忍依賴(lài)（圖10中的FT1和FT2）。根據(jù)依賴(lài)關(guān)系，該組件可能會(huì)向外傳播錯(cuò)誤，但并不能接收外來(lái)錯(cuò)誤。

5.3 模型轉(zhuǎn)化及結(jié)果分析

圖12是上述錯(cuò)誤模型根據(jù)之前提到的轉(zhuǎn)化規(guī)則轉(zhuǎn)化得到的IMC 模型，其中，Restart示線(xiàn)程重啟，重新回到Error＿Free狀態(tài)。圖13 中，該事件的發(fā)生也對(duì)系統(tǒng)產(chǎn)生影響：當(dāng)FP＿Comp1 發(fā)生錯(cuò)誤，系統(tǒng)則使用備用操作模塊FP＿Comp2；當(dāng)FP＿Comp1重啟之后，回到Error＿Free狀態(tài)，系統(tǒng)重新使用主要操作模塊FP＿Comp1。FP＿Comp2 向RDunit傳播錯(cuò)誤的部分與FP＿Comp1相同，所以我們將其省略。

表2是圖中對(duì)應(yīng)的轉(zhuǎn)換率和概率的具體數(shù)值，λc是總線(xiàn)的故障率。通過(guò)圖12的IMC模型，結(jié)合IMC分析方法，可以得出兩種備選方案的故障率與總線(xiàn)故障率λc的關(guān)系，如表3所示。從結(jié)果中可以看出，當(dāng)λc＜10－5/h時(shí)，兩種備選方案的故障率比較接近；當(dāng)λc＞10－5/h時(shí)，方案a相較方案b，故障率明顯提高。這是因?yàn)榉桨竍在正常情況下，F(xiàn)Punit與RDunit處于同一臺(tái)處理器，數(shù)據(jù)處理不經(jīng)過(guò)總線(xiàn)，受總線(xiàn)故障影響較小。所以，當(dāng)總線(xiàn)故障率λc＞10－5/h時(shí)，選用方案b比較合適。

Figure 11 Error model of the FPunit圖11 FPunit的錯(cuò)誤模型

Figure 12 IMC model of the system圖12 系統(tǒng)IMC模型

Table 2 Nominal value of the transition rates表2 AADL轉(zhuǎn)換率的標(biāo)準(zhǔn)值

Table 3 Experimental results表3 實(shí)驗(yàn)結(jié)果

Figure 13 Impact of errors on the system model圖13 錯(cuò)誤對(duì)系統(tǒng)模型產(chǎn)生的影響

6 結(jié)束語(yǔ)

本文提出了一種從AADL可靠性模型向IMC模型轉(zhuǎn)化的方法，并給出具體的轉(zhuǎn)化規(guī)則。以這些規(guī)則為基礎(chǔ)，通過(guò)一個(gè)空中交通控制系統(tǒng)的實(shí)例，證明轉(zhuǎn)化規(guī)則的可用性；對(duì)AADL可靠性模型進(jìn)行了定量分析，對(duì)系統(tǒng)模型的建立提出參考意見(jiàn)，也給AADL可靠性模型分析提供了一種新的思路。

雖然本文在AADL可靠性模型分析上提出了一種創(chuàng)新，提出了新的轉(zhuǎn)化規(guī)則，但是AADL語(yǔ)言還在不斷更新其語(yǔ)法標(biāo)準(zhǔn)，添加新的語(yǔ)法元素和規(guī)則。后期的工作和研究重點(diǎn)在于隨著AADL標(biāo)準(zhǔn)的更新擴(kuò)充相應(yīng)的AADL 可靠性模型到IMC 計(jì)算模型的模型轉(zhuǎn)換規(guī)則。同時(shí)，這種轉(zhuǎn)換方法尚未實(shí)現(xiàn)自動(dòng)化，這也是今后工作的重點(diǎn)。

［1］ OMG.Model driven architecture（MDA）［EB/OL］.［2010－07－03］.http：//www.omg.org/mda/.

［2］ Feiler P H，Gluch D P，Hudak J J.The architecture analysis＆design language（AADL）：An introduction：CMU/SEI－2006－TN－011［R］.Pittsburgh：Carnegie－Mellon University，2006.

［3］ Yang Z B，Pi L，Hu K，et al.AADL：An architecture design and analysis language for complex embedded real－time systems［J］.Journal of Software，2010，21（5）：899－915.（in Chinese）

［4］ SAE－AS5506/1：SAE architecture analysis and design language（AADL）Annex vol.1，Annex E：Error Model Annex［Z］.Warrendale，PA，USA：International Society of Automotive Engineers，2006.

［5］ Rugina A E，Kanoun K，Kaaniche M.A system dependability modeling framework using AADL and GSPNs［M］∥Architecting Dependable Systems IV.Berlin：Springer，2007：14－38.

［6］ Hermanns H.Interactive Markov chains and the quest for quantified quality［M］.Berlin，Germany：Springer－Verlag，2002.

［7］ SEI AADL Team.An extensible open source AADL tool environment（OSATE）［EB/OL］.［2006－06－02］.http：//la.sei.cmu.edu/aadl/downloads/osate13/AADLTooIUserGuide1.3.0%202006－06－02.pdf.

［8］ Varona－Gómez R，Villar E.AADL simulation and performance analysis in SystemC［C］∥Proc of the 14th IEEE International Conference on Engineering of Complex Computer Systems，2009：323－328.

［9］ Hecht M，Lam A，Vogl C.A tool set for integrated software and hardware dependability analysis using the architecture analysis and design language（AADL）and error model annex［C］∥Proc of the 16th IEEE International Conference on Engineering of Complex Computer Systems（ICECCS），2011：361－366.

［10］ Wang Geng，Zhou，Xing－she，Zhang Fan，et al.Research on model－based testing on AADL［J］.Computer Science，2009，36（11）：127－130.（in Chinese）

［11］ LI Zhen－song，Gu Bin.Research on verification method of AADL behavior model based on UPPAAL［J］.Computer Science，2012，39（2）：159－161.（in Chinese）

［12］ Liu Q，Gui S L，Li Y.Schedulability verification of AADL model based on UPPAAL［J］.Computer Applications，2009，29（7）：1820－1824.（in Chinese）

［13］ Zhang C，Yang Z，Dong Y.Research and assessment of the reliability of a fault tolerant model using AADL［C］∥Proc of Advanced Software Engineering and its Applications，2008：45－52.

［14］ Dong Y W，Wang G R，Zhang F，et al.Reliability analysis and assessment tool for AADL model［J］.Journal of Software，2011，22（6）：1252－1266.（in Chinese）

附中文參考文獻(xiàn)：

［3］ 楊志斌，皮磊，胡凱，等.復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)與分析語(yǔ)言：AADL［J］.軟件學(xué)報(bào)，2010，21（5）：899－915.

［10］ 王庚，周興社，張凡，等.AADL 模型的測(cè)試方法研究［J］.計(jì)算機(jī)科學(xué)，2009，36（11）：127－130.

［11］ 李振松，顧斌.基于UPPAAL 的AADL 行為模型驗(yàn)證方法研究［J］.計(jì)算機(jī)科學(xué)，2012，39（2）：159－161.

［12］ 劉倩，桂盛霖，李允，等.基于UPPAAL的AADL模型可調(diào)度性驗(yàn)證［J］.計(jì)算機(jī)應(yīng)用，2009，29（7）：1820－1824.

［14］ 董云衛(wèi)，王廣仁，張凡，等.AADL 模型可靠性分析評(píng)估工具［J］.軟件學(xué)報(bào)，2011，22（6）：1252－1266.