基于AADL模型航空安全軟件可信性度量方法

劉歆寧,康 玲

(大連東軟信息學院 軟件工程系,遼寧 大連 116023)

0 引 言

近年來,隨著安全關鍵軟件在航空航天領域的廣泛應用,安全關鍵軟件在兼顧高可靠性和高安全性的需求不斷提高,同時安全關鍵軟件也面臨著越來越復雜的窘境。近年來,模型驅動開發方法逐漸成為安全關鍵軟件開發方法的一種發展趨勢,例如國際民航領域使用的機載系統適航審定中的軟件開發標準DO-178C就將模型驅動和形式化方法作為其核心標準的重要技術補充[1]。

美國自動機協會(Society of Automotive Engineers,SAE)體系結構描述語言附屬委員會、嵌入式計算系統委員會及航空電子系統公司于2004年10月提出了專門針對安全關鍵的嵌入式實時系統的軟硬件分析設計語言─體系結構分析與設計語言(Architecture Analysis and Design Language,AADL)[2]。AADL能夠對嵌入式軟件的功能和非功能屬性進行建模和分析,是控制系統復雜性和保證軟件質量的重要手段。目前,對基于AADL模型的軟件可信性度量與分析,主要集中于將AADL故障模型附件轉換為隨機Petri網或故障樹的方法[3-5],以實現對模型的可靠性分析,因此,研究全面的可信性的度量與分析方法是十分必要的。

基于以上考慮,該文提出了基于AADL模型的軟件可信性的度量與分析技術的研究這一課題。該研究能夠在軟件開發的早期階段對基于AADL模型的軟件可信性進行度量、分析與評估,從而提高軟件的質量。該文研究AADL模型特點,從AADL模型中提取可度量的指標并建立度量模型,將對象軟件度量方法、軟件體系結構度量方法、Markov分析方法及熵理論方法應用于各個度量指標的計算之中,對度量結果進行分析,并根據所建立的軟件可信性度量模型,采用適合的評估方法對軟件可信性的度量結果進行評估。最終實現一個基于AADL模型的軟件可信性度量與評估的工具,該工具能夠分析已有軟件的AADL模型,提取模型中的可信性度量指標并計算指標值,對度量結果進行簡單的分析并最終對度量結果進行評估。

1 基礎理論

1.1 AADL標準及擴展附件

為了更好地設計與分析嵌入式實時系統的軟、硬件體系結構及功能與非功能屬性,嵌入式實時系統體系結構分析與設計語言(AADL)被提出。AADL標準由核心語言標準和擴展附件標準組成,是一種基于組件的建模語言,采用結構化的描述來對嵌入式系統的軟硬件進行統一建模。

AADL的擴展附件是對AADL核心標準的補充描述,它們可以嵌入在AADL核心語言的包以及組件實現中。其中比較重要和常用的附件是故障模型附件EMA(Error Model Annex)和行為附件BA(Behavior Annex)。AADL故障模型由類型和實現兩部分組成。故障模型類型(error model type)定義了故障狀態(error states)、故障事件(error events)以及故障傳播(error propagations)等,其中故障事件是針對組件內部的,故障傳播則是針對組件之間交互的[6-7]。

1.2 軟件可信性度量與分析技術

對于可信性的概念,不同的人員有不同的認識。微軟的比爾蓋茨提出了可信計算的4個基本屬性[8],即可靠性、安全性、保密性和商業誠信。美國科學與技術委員會則認為:可信系統要求具有很多特性,包括功能正確性、防危性、容錯性、實時性和安全性。陳火旺院士提出了高可信性質的概念[9],認為軟件系統的可信性質是指該系統需要滿足的關鍵性質。國際標準ISO/IEC 9126:2001[10]定義了軟件的質量模型,該模型將軟件質量屬性劃分為6個特性:功能性、可靠性、易用性、效率、維護性和可移植性。劉晗從源代碼證據入手,建立面向航天領域的嵌入式軟件可信度量評估方法[11]。

1.3 模糊綜合評價法

模糊綜合評價法[12]是一種基于模糊數學的綜合評價方法。該綜合評價法根據模糊數學的隸屬度理論把定性評價轉化為定量評價,即用模糊數學對受到多種因素制約的事物或對象做出一個總體的評價[12]。此方法具有結果清晰、系統性強的特點,能較好地解決模糊的、難以量化以及各種非確定性的問題。

1.4 基于AADL模型軟件可信性度量系統研究框架

目前基于AADL模型的度量與分析主要集中在利用AADL故障模型的可靠性度量,對AADL核心模型的度量涉獵極少。AADL核心標準描述了AADL的功能和非功能屬性,這些屬性直接影響到軟件的可信性,因此對其進行度量是十分必要的。并且目前對AADL模型的度量主要是從可靠性和安全性兩個角度進行,而僅這兩個方面是不能全面反映軟件在可信性方面存在的問題的。同時,缺少基于AADL模型的軟件可信性度量與評估工具。

2 基于AADL航空軟件可信性度量

2.1 核心模型的軟件可信性度量方法

2.1.1 AADL核心模型復雜性度量

軟件復雜度度量作為軟件工程的重要組成部分,可為高質量軟件的研究提供支撐[13]。組件之間存在依賴關系,則被依賴組件的變化將影響到依賴于它的組件。顯然,組件之間的依賴關系越多,組件之間的相互影響越大,系統復雜性越高。

模式modes是AADL核心模型所特有的,它用來描述運行時體系結構的動態演化。通過分析模式modes的特點,可得到如下幾個度量指標:

指標一:平均模式轉換總數(Average Number of Mode Transitions,ANMT)。

定義NMT(i)為第i個有模式轉換組件的模式轉換總數,則ANMT的計算方法如公式(1)所示:

(1)

其中,n為有模式轉換的組件的總數。

度量原則:ANMT越大,組件在不同的模式之間轉換次數越多,則系統的復雜性越高。

指標二:系統所含有模式轉換的子組件數(Number of Modes in System,NMS)。

在AADL核心模型中,使用in modes語句指定一個子組件在模式modes中是活躍的,則NMS為所有含有模式轉換的子組件總數。

度量原則:NMS越大,則該子組件的職責越多,整個系統也就越復雜。

由本節度量指標的計算方法,得到計算模式復雜性所涉及的AADL核心模型的元素與所使用的度量方法的對應關系,如表1所示。

表1 模式復雜性度量與度量方法對應關系

AADL核心模型中的包與面向對象中的包的概念相似,通過引入一個獨一無二名字空間,提供了一個方式來組織組件類型、組件實現及特性組等元素。本節通過對AADL核心模型中包的分析,從中提取出以下幾個度量指標:

指標一:平均包中關聯關系的總數(Average Number of Associations in a Package,ANAP)。

在AADL核心模型的每個包中,組件及組件之間的連接connections描述了系統的組成和結構,體現了軟件體系結構的主要信息。從這個方面考慮,定義NAP為包中connections的總數,則ANAP的計算方法如公式(2)所示:

(2)

其中,NAP(i)為第i個包的NAP值,n為包總數。

度量原則:ANAP越大,包復雜性越高。

指標二:平均包中的關聯關系數(NAP)與包中組件的數目的比值(Average Number of Associations vs.Component in a Package,ANAVCP)。

包中平均每個組件的關聯關系越多,包就越復雜,從而導致包越難理解和維護,則:

(3)

其中,NAP為包中的關聯數,compn為包中的組件數,則ANAVCP的計算方法如公式(4)所示:

(4)

其中,NAVCP(i)為第i個包的NAVCP值,n為包的數目。

度量原則:ANAVCP越大,包復雜性越高。

由本節度量指標的計算方法,得到計算包復雜性所涉及的AADL核心模型的元素與所使用的度量方法的對應關系,如表2所示。

表2 包復雜性度量與度量方法對應關系

2.1.2 AADL核心模型耦合性度量

耦合性度量是軟件結構中各個模塊之間聯系緊密程度的度量。耦合性越高表示該元素與其它元素的調用關系越多,則該元素設計改動的敏感性越明顯,這給軟件的維護和修改造成了困難[14]。因此,組件間的耦合性可用來度量組件的可理解性、可靠性、可維護性和可用性等。本部分針對AADL核心模型的特點,分別從連接connections、特性features、繼承extends和包package的角度考慮,提取出以下度量指標:

指標一:平均繼承耦合(Average Extends Coupling,AEC)。

定義EC(i)為系統中所有從組件i繼承而來的組件的信息量的集合,則AEC的計算方法如公式(5)所示:

(5)

其中,n為繼承父組件的個數。

度量原則:AEC越大,繼承父組件與繼承子組件之間的關聯越密切,耦合度越高。

指標二:包間耦合因子(Coupling Factor between Packages,CFP)。

如果包ci使用了包cj中的屬性或特性,則isclient(ci,cj)=1,否則isclient(ci,cj)=0,則CFP的計算方法如公式(6)所示:

(6)

其中,TC表示系統的包的總數。

度量原則:包間耦合因子越大,包之間的關聯越密切,耦合度越高。

由本節度量指標的計算方法,得到計算耦合性所涉及的AADL核心模型的元素與所使用的度量方法的對應關系如表3所示。

表3 耦合性度量與度量方法對應關系

2.2 基于AADL故障模型的軟件可信性度量方法

AADL故障模型附件是一種半形式化的語言,直接對基于AADL故障模型的軟件進行可信性度量是比較困難的,而形式化方法可以對語義進行更加精細的描述,能夠更好地用于模型的可信性分析,為此需要考慮對AADL故障模型進行形式化的語義描述。

2.2.1 AADL故障模型到Markov模型的轉化規則

通過對AADL故障模型的研究可知,AADL故障模型同Markov模型相同,都是指明了狀態和狀態的轉移,即故障狀態及故障狀態之間的轉移,一個故障狀態轉移到其他故障狀態的概率值由Occurrence屬性指明。將AADL故障模型轉換為Markov模型,是模型轉換的過程,通過對AADL故障模型和Markov模型進行分析,得到將AADL故障模型轉化為Markov模型的整體規則是:將AADL故障模型中組件的故障狀態對應于Markov模型中的狀態,故障狀態遷移對應于Markov模型中的狀態遷移,故障狀態遷移的Occurrence屬性值對應于Markov模型中狀態遷移的概率。為了體現AADL故障模型的相關信息,在傳統的Markov模型的形式化定義的基礎上,提出了一種擴展的Markov鏈:

定義1 擴展Markov鏈(Expanded Markov Chain,EMC):EMC=(S,S0,∑,P,Q),其中:

(1)S是組件的故障狀態的集合,是一個有限集,可表示成:S={S0,S1,…,Sn};

(2)S0是組件的初始故障狀態,一般是無故障狀態,且S0∈S;

(3)∑是故障狀態轉移集合,每一個集合用一個兩元組表示:{TriggerType,TriggerName},其中TriggerType是觸發故障狀態轉移的類型,此類型包括故障事件error event和故障傳播error propagation兩種,該文只考慮故障事件error event,對于故障傳播error propagation在以后的研究中再將其考慮在內,故此處的類型均為故障事件error event ,TriggerName是觸發故障狀態轉移的事件的名字;

(4)P是故障狀態之間轉移的概率集,每一個概率集定義為一個三元組:{Probability,ProbabilityType,ProbabilityDefinition},其中Probability是故障狀態轉移的概率,ProbabilityType指明是失效率還是恢復率,分別用failure rate和recovery rate表示;ProbabilityDefinition指明轉移的概率是服從1-e-λ的指數分布,還是一個0～1的小數值,分別用poisson和fixed表示;

(5)Q表示故障狀態之間轉移的關系,即:

S×∑→S

根據定義1的基于AADL故障模型的擴展Markov鏈的形式化描述,將AADL故障模型的各個元素與擴展的Markov模型中的各個元素相對應,得到AADL故障模型到擴展Markov鏈的對應關系,如表4所示。

表4 AADL故障模型的元素與擴展Markov鏈的元素的對應關系

圖1是一個組件的AADL故障模型實例,將它用上文提出的轉換規則轉換為擴展的Markov鏈如下:

圖1 故障模型實例

EMC={S,Error_Free,∑,P,Q},其中:

S={Error_Free,Erroneous,Failed};

∑={∑1,∑2,∑3,∑4},其中∑1={error event,Perm_Falult},∑2={error event,Temp_Fault },∑3={error event,Restart},∑4={error event,Recover}

P={P1,P2,P3,P4},其中P1={0.125,failure rate,fixed},P2={0.175,failure rate,fixed},P3={0.8,recovery rate,fixed},P4={0.9,recovery rate,fixed}

Q={Error_Free×∑1→Failed,Error_Free×∑2→Erroneous,Failed×∑3→Error_Free,Erroneous×∑4→Error_Free }

2.2.2 AADL故障模型的可信性度量

從AADL故障模型的Markov形式化描述中,可以獲取從無故障狀態到故障狀態的失效率,以及故障狀態到無故障狀態的恢復率,從而得到一步狀態轉移概率矩陣。AADL故障模型之間的狀態轉移滿足Markov鏈的齊次性,因此由AADL故障模型轉換的擴展Markov鏈也是齊次的,因此可采用Markov分析方法預測組件在長期運行后的失效率。以圖1的AADL故障模型為例,該模型有一個初始無故障狀態和兩個故障狀態,可轉換為三態的Markov鏈,其一步狀態轉移概率矩陣P如公式(7)所示:

(7)

設穩態狀態向量為Y(3)={y1,y2,y3},其中y1為組件長期運行時處于正常狀態的概率,y2和y3分別為組件長期運行時處于兩個故障狀態的概率,則y2+y3為組件長期運行時的總體失效率,即穩態失效率。由方程組(8)得:

(8)

計算出單個組件的相關度量指標之后,通過指定各個組件的權重,可以得到系統的相關的度量指標如下:

(1)系統的穩態失效率為:

(9)

其中,λi為第i個組件的穩態失效率,Simpi為第i個組件的權重,且該指標與軟件可信性是負相關。

(2)系統的恢復率為:

(10)

其中,μi為第i個組件的恢復率,Simpi為第i個組件的權重,μi的值通過從第i個組件的AADL核心模型中的屬性集中提取出來,且該指標與軟件可信性是正相關。

(3)系統的MTBF為:

(11)

其中,MTBFi為第i個組件的MTBF,Simpi為第i個組件的權重,且該指標與軟件可信性是正相關。

(4)通過Markov分析方法,可以求出系統的可用度。可用度是指系統在任一隨機時刻處于工作或可使用狀態的概率,它是系統效能的重要因素。當Markov鏈是齊次的,且系統的穩態失效率和恢復率分別為λsum和μsum時,系統的瞬態可用度為:

(12)

當t→∞時,可得系統的穩態可用度為:

(13)

3 基于AADL模型的軟件可信性度量模型與評估方法

在對軟件進行可信性評估之前,可以對軟件可信性進行一些簡單的分析,總結2.1與2.2中AADL模型可信性度量的研究成果,得到基于AADL模型的質量屬性相關的度量指標列表,如表5所示。

表5 AADL質量屬性相關的指標列表

除了對度量結果進行如上的定性分析,還可以利用AADL模型中的屬性集property sets對度量結果進行定量分析。AADL模型中的屬性properties定義了組件以及組件描述的約束,用戶可根據自己的需求對屬性properties進行擴展,這些屬性主要定義了系統的質量屬性方面的約束,文中的用戶可以為設計人員或者相關領域專家。

將各個度量指標值與屬性集中相應屬性的屬性值相比較,有如下兩種情況:

(1)度量指標與可信屬性成正相關時:當度量指標值大于屬性值時,該度量指標值滿足用戶需求;當度量指標值小于屬性值時,該度量指標不滿足用戶需求;

(2)度量指標與可信屬性成負相關時:當度量指標值小于屬性值時,該度量指標值滿足用戶需求;當度量指標值大于屬性值時,該度量指標不滿足用戶需求。

這樣,設計人員可以根據分析結果對所設計的模型進行修改,使模型盡可能地滿足用戶的需求。

4 工具實現及案例分析

4.1 工具實現

基于AADL模型軟件可信性度量與評估工具的目標是對基于AADL模型的軟件可信性進行度量、分析與評估。該工具組件給予基于AADL模型的軟件可信性度量、分析與評估的全方位支持,能夠在軟件開發早期為相關人員做出決策提供參考。

該工具包括基于AADL模型的軟件可信性度量模型的定制、AADL數據采集、AADL模型的可信性度量與分析及AADL模型的可信性評估四個模塊,見圖2。工具首先需要通過數據采集模塊采集度量數據,解析以XML形式表示的AADL模型,從模型文件中提取被度量組件及組件之間的關系,以實現對這些被度量組件的解析。

圖2 基于AADL模型的軟件可信性度量與評估系統體系結構

AADL模型度量與分析模塊以定制的可信性度量模型為依托,統計采集到的數據,度量與分析統計的結果可以反映出軟件的可信性。系統對采集的數據進行度量后,將度量的指標值傳遞給軟件可信性評估模塊。

4.2 案例分析

本節以一個應用實例來詳細介紹基于AADL模型的軟件可信性度量與評估工具的操作步驟和實驗結果。該課題以AADL官方網站上的航空電子系統Avionics_System為例。針對該航空電子系統Avionics_System中的主要組件,根據以往的經驗,給出了相應的故障模型,并給出了屬性集。圖3顯示了航空電子系統Avionics_System的圖形表示,由于系統中的端口交互較為復雜,圖3只給出了系統的主要結構。

圖3 航空電子系統模型

進入基于AADL模型的軟件可信性度量與評估工具主界面。本節以航空電子系統Avionics_System為例,按照可信性度量模型定制->AADL數據采集->AADL模型度量與分析->AADL模型評估的操作步驟對該工具進行介紹,并對系統運行的結果進行分析和總結。

(1)可信性度量模型定制。

通過系統結構樹中的可信性度量模型定制節點,進入基于AADL模型的軟件可信性度量與評估工具的可信性度量模型定制功能,用戶可以根據實際需要或自身經驗定制軟件的度量模型。

(2)AADL模型數據采集。

軟件可信性度量模型定制完成后,進入AADL數據采集界面,該模塊包括3個子模塊:AADL核心模型數據采集、AADL故障模型數據采集和AADL屬性集采集。

(3)AADL模型度量與分析。

通過采集AADL模型數據并對AADL模型進行解析之后,該工具可以對AADL模型進行度量與分析,該度量與分析由兩方面組成,即AADL核心模型度量與分析和AADL故障模型度量與分析。

(4)AADL模型評估。

根據評價矩陣建立的方法,該部分針對各個度量指標設定隸屬函數中的μ值,從而計算出各個度量指標在各個可信等級上的隸屬度,進而得到該航空電子系統Avionics_System隸屬于各個可信等級的結果。從圖4中的結果可以看出,評估結果對應可信第一級“肯定可信”隸屬度最大,第二、三級“很可能可信”的隸屬度明顯低于第一級,第四、五級的隸屬度很低,該結果表明該航空電子系統Avionics_System屬于五個可信等級中的第一等級。

圖4 航空電子系統可信性評估結果

若對該飛行Avionics_System的AADL模型的某一方面進行修改,如修改該系統的故障模型的概率轉移值,其他條件不變,最終得到軟件可信等級隸屬度和最終系統可信性評估結果。從圖5中可以看到:與修改之前相比,該系統在第一等級的隸屬度有所降低,在第四、五級的隸屬度有顯著增加。這說明對被評估模型的任意一個方面修改都能夠影響軟件可信性評估結果,說明該工具是敏感的。

圖5 修改模型后系統可信性評估結果

(5)實驗結果。

該工具實現了對基于航空電子系統Avionics_System的AADL模型進行可信性度量、分析與評估的功能,對實驗結果的分析表明:利用該工具可以對基于AADL模型的軟件進行可信性度量、分析與評估,得到的度量與評估結果可供設計人員參考,以便在軟件開發早期發現軟件可信性方面存在的問題,從而提高軟件的質量。利用該工具對軟件進行可信性度量、分析與評估的步驟簡單便捷,用戶可以很快熟練使用該工具。

5 結束語

基于AADL的核心語義和AADL故障模型,提出了一種軟件可信性度量與評估方法,由于時間和工作量的限制,方法的研究與工具的實現還存在不足,進一步的工作應該從以下幾個方面展開:

(1)對基于AADL故障模型的度量進行更深入的研究,將其轉換為其他形式化模型以提取更多體現軟件可信屬性的度量指標。

(2)對軟件可信性進行評估時,存在歷史數據嚴重不足的問題,因此公式的參數可能存在不準確的問題,下一步將收集歷史數據來進一步驗證公式。

(3)對AADL的行為附件behavior annex進行研究,提取出可度量的指標,完善基于AADL模型的軟件可信性度量與分析模型的指標體系,從而能夠更全面且充分地對軟件可信性進行度量與評估。