劉 晗， 陶紅偉， 陳儀香*

1. 華東師范大學(xué)軟件工程學(xué)院，教育部軟硬件協(xié)同設(shè)計技術(shù)與應(yīng)用工程研究中心，上海 200062 2. 鄭州輕工業(yè)大學(xué)計算機(jī)與通信工程學(xué)院，鄭州 450002

0 引 言

近年來，航天技術(shù)迅猛發(fā)展，軟件作為航天技術(shù)中必不可少的部分，其功能越來越復(fù)雜，規(guī)模越來越大，航天軟件已經(jīng)成為人們關(guān)注和研究的重點之一.但是，作為安全攸關(guān)領(lǐng)域，航天軟件日益復(fù)雜化帶來很多潛在安全問題，一旦軟件發(fā)生事故，其損失無法估計.因此，航天軟件可信性研究不容忽視.

自1972年Anderson JP首次提出可信系統(tǒng)的概念[1]，人們便開始研究可信系統(tǒng).早期，人們對可信系統(tǒng)的研究主要集中在硬件環(huán)境和操作系統(tǒng)，直到美國國防部首先在可信計算機(jī)系統(tǒng)測評標(biāo)準(zhǔn)中提出可信計算機(jī)系統(tǒng)的軟件也要是可信的[2]，人們才更加關(guān)注軟件可信性.此后，LAPRIE[3]給出軟件可信性與可靠性的區(qū)別，認(rèn)為軟件可靠性是可信性的一個子集，可信性比可靠性復(fù)雜得多.美國科學(xué)與技術(shù)委員會 (national science and technology council, NSTC)也在之后提出高可信系統(tǒng)[4]，他們認(rèn)為高可信系統(tǒng)主要關(guān)注功能正確性、防危性、容錯性、實時性和安全性等性質(zhì)，并且他們強(qiáng)調(diào)用戶體驗，認(rèn)為高可信系統(tǒng)必須能在任何情況下都能按照用戶預(yù)期的情況運(yùn)行.美國國家研究委員會(national research council, NRC)也認(rèn)為可信系統(tǒng)需要強(qiáng)調(diào)用戶體驗，可信系統(tǒng)必須在任何情況下都能按照用戶預(yù)期的目標(biāo)運(yùn)行，但是他們提出的可信定義主要關(guān)注正確性、私密性、可靠性、防危性、可生存性和安全性，其中安全性包括機(jī)密性、完整性、可用性[5].德國奧爾登堡大學(xué)可信軟件研究院在2006年提出軟件可信性應(yīng)該包括正確性、安全性、服務(wù)質(zhì)量、保密性和隱私性，其中服務(wù)質(zhì)量又包括可用性、可靠性和性能[6].

我國自2000年以來也有很多軟件可信研究團(tuán)隊提出了軟件可信性定義.陳火旺院士認(rèn)為高可信性質(zhì)包括可靠性、防危性、安全性、可生存性、容錯性和實時性[7].劉克等[8]也認(rèn)為可信性是軟件諸多屬性的綜合反映，提出可信軟件是指軟件系統(tǒng)的動態(tài)運(yùn)行及其結(jié)果總是符合人們預(yù)期，并且在受到干擾時仍能提供連續(xù)服務(wù).

由于軟件可信性是多種屬性的綜合反映，對其量化評估往往非常困難.國內(nèi)外學(xué)者從各種不同角度提出一系列方法來度量評估軟件可信性.SANDRO等[9]通過將問卷調(diào)查和多元統(tǒng)計分析技術(shù)相結(jié)合的方法，建立兼顧主觀評價和客觀度量的軟件可信性度量模型.美國國家標(biāo)準(zhǔn)與技術(shù)研究院(National Institute of Standards and Technology, NIST)提出一個評估軟件可信性的初步框架，它以自上而下的方式，使用形式化的方法得出可信因素的確切數(shù)值[10-12].ALEXOPOULOS等[13]以貝葉斯概率和Dempster-Shafer證據(jù)理論為基礎(chǔ)，提出M-STAR模塊化軟件可信性體系結(jié)構(gòu)框架.JIN等[14]提出一個可容納四個子度量標(biāo)準(zhǔn)的系統(tǒng)級信任度度量標(biāo)準(zhǔn)框架STRAM，該框架提供一種分層結(jié)構(gòu)，其中每個子度量定義一個子本體.

國內(nèi)許多研究團(tuán)隊同樣在軟件可信性度量領(lǐng)域取得系列成果.鄭志明院士和李未院士等人將動力學(xué)統(tǒng)計分析引入到軟件可信性度量，通過動力學(xué)基本方法研究軟件可信性及其演化過程[15-17].楊善林院士等[18]將效用理論和Dempster-Shafer證據(jù)理論相結(jié)合，提出一種基于可信指標(biāo)樹的證據(jù)推理算法.王懷民院士等[19]提出一種分層的軟件可信分級模型，并通過驗證方法對軟件進(jìn)行評估.沈昌祥院士從軟件行為角度出發(fā)，提出基于并發(fā)理論的軟件可信性度量方法[20-21].王德鑫等[22]則專注于軟件過程，將可信證據(jù)融入軟件開發(fā)的全過程，建立基于過程的軟件可信度評估方法.田俊峰等[23]通過檢查點來捕獲軟件行為軌跡，并通過機(jī)器學(xué)習(xí)和余弦相似性的方法來預(yù)測軟件可信性.陳儀香等[24]則基于公理化方法，將軟件屬性進(jìn)行分解，提出基于屬性分解的軟件可信度量模型.此外，陳儀香等人還通過Extensive結(jié)構(gòu)，研究了面向源代碼的軟件可信性度量模型.

本文在文獻(xiàn)[24]的基礎(chǔ)上，從源代碼角度入手，建立面向航天型號軟件C語言可信證據(jù)規(guī)范，該證據(jù)規(guī)范區(qū)分關(guān)鍵證據(jù)和非關(guān)鍵證據(jù)以及可信正證據(jù)與可信負(fù)證據(jù).此外，本文提出了一種面向源代碼可信證據(jù)的航天軟件可信度量模型和可信性分級模型，最后，本文在NASA開源軟件Core Flight Executive 上驗證了度量方法的有效性和實用性.

1 軟件失效模型與可信證據(jù)

1.1 軟件失效模型

文獻(xiàn)[25]中指出軟件失效是指程序動態(tài)運(yùn)行結(jié)果與預(yù)期結(jié)果不一致，這種情況是在軟件運(yùn)行過程中觸發(fā)軟件缺陷造成的.為了更好地描述這一過程，本文首先給出一個軟件失效模型來描述不同因素對軟件失效的影響，如圖1所示.

圖1 軟件失效模型Fig.1 Software failure model

軟件在編碼開發(fā)過程中難免會留下一些缺陷，這些缺陷在正常情況下不會影響軟件的預(yù)期功能，隨著時間的推移或者在某些外部干擾情況下，這些缺陷極有可能被激活，成為錯誤，導(dǎo)致軟件失效，從而使得軟件失信，其可信性降低.

1.2 可信證據(jù)

國防科技大學(xué)的Trustie團(tuán)隊在文獻(xiàn)[26]中給出可信證據(jù)的一種定義，該定義指出任何與軟件相關(guān)并能反映其某種可信屬性的數(shù)據(jù)、文檔或者其他信息都稱為軟件可信證據(jù).

由此可見，可信證據(jù)是軟件可信性的反映，而軟件可信性由軟件諸多屬性的綜合構(gòu)成.本文主要面向源代碼來度量軟件可信性，因此，本文將軟件代碼中用來衡量軟件可信性的指標(biāo)依據(jù)定義為可信證據(jù).

定義1(源代碼可信證據(jù)).源代碼可信證據(jù)是指在軟件源代碼中用來衡量軟件可信性指標(biāo)的依據(jù)，包括表達(dá)式類可信證據(jù)、聲明定義類可信證據(jù)、語句類可信證據(jù)和參數(shù)注釋類可信證據(jù).

不同的可信證據(jù)對軟件可信性有著不同的影響，有些可信證據(jù)的出現(xiàn)可能會對軟件產(chǎn)生致命的影響，例如，航天類軟件代碼中一旦出現(xiàn)數(shù)組越界情況，軟件的運(yùn)行便很可能偏離用戶預(yù)期.鑒于此，本文把證據(jù)分為關(guān)鍵證據(jù)和非關(guān)鍵證據(jù)，用來區(qū)分不同證據(jù)對軟件可信性的影響.

定義2(關(guān)鍵證據(jù)與非關(guān)鍵證據(jù)).關(guān)鍵證據(jù)是指源代碼中一旦出現(xiàn)或缺失會對軟件產(chǎn)生巨大影響的可信證據(jù)，非關(guān)鍵證據(jù)是除關(guān)鍵證據(jù)外的所有可信證據(jù)，其出現(xiàn)或缺失不會對軟件產(chǎn)生致命影響.

對于不同類別、不同應(yīng)用場景的軟件，用戶所期望的預(yù)期結(jié)果往往不同，相應(yīng)源代碼中會產(chǎn)生致命影響的證據(jù)也不完全相同，很難通過統(tǒng)一的關(guān)鍵證據(jù)集來衡量.因此，不同類型的軟件需要根據(jù)軟件自身的特性來定義關(guān)鍵證據(jù)和非關(guān)鍵證據(jù).表1展示了三個不同類別軟件的關(guān)鍵證據(jù).

表1 關(guān)鍵證據(jù)示例Tab.1 Examples of key evidence

通過關(guān)鍵證據(jù)和非關(guān)鍵證據(jù)，可以區(qū)分不同證據(jù)對軟件可信性的不同程度影響，并且可以建立應(yīng)用于不同領(lǐng)域的可信證據(jù).

此外，可信證據(jù)對軟件可信性的影響還有正面和負(fù)面兩種.因此本文還將可信證據(jù)分為正證據(jù)和負(fù)證據(jù)，正證據(jù)對軟件可信性有著正面影響，負(fù)證據(jù)對軟件可信性有著負(fù)面影響.

在軟件失效過程中，代碼中存在的缺陷可以被防護(hù)或者可以減輕其影響使得程序按照預(yù)期運(yùn)行.這些防護(hù)措施或者減輕缺陷影響的方法的可信證據(jù)即為正證據(jù).

定義3(正證據(jù)).正證據(jù)是指在源代碼中所有對缺陷進(jìn)行防護(hù)或者使得缺陷不影響程序按照預(yù)期運(yùn)行的可信證據(jù)，它與軟件可信性正相關(guān)，防護(hù)缺陷程度越高或者使得缺陷不影響程序按照預(yù)期運(yùn)行的能力越大，軟件可信性就越高.正證據(jù)可以用如下的三元組表示：

PositiveEvidence=

其中，Name表示正證據(jù)的名稱，Metric表示正證據(jù)的度量元，分別用A、B、C、D四個等級表示，每一等級包含不同要求，MetricValue表示正證據(jù)的度量值，取值范圍為[1,10]，由度量元的評級映射得到，其中A級映射為10，B級映射為7，C級映射為4，D級映射為1.例如，表2展示了Name為“過程體、循環(huán)體、then/else中語句必須用括號括起”的正證據(jù).

表2 正證據(jù)示例Tab.2 An example of positive evidence

代碼的缺陷受到外部干擾或者隨著時間推移，這些缺陷在沒有防護(hù)的情況下就可能導(dǎo)致軟件失效，從而使得軟件失信，這些缺陷所對應(yīng)的證據(jù)即為負(fù)證據(jù).

定義4(負(fù)證據(jù)).負(fù)證據(jù)是指隱藏在源代碼中使得軟件受到外部干擾和時間推移可能導(dǎo)致軟件失信的證據(jù)，它與軟件的可信性負(fù)相關(guān)，其風(fēng)險程度越高，出現(xiàn)的次數(shù)越多，軟件的可信性越低，可以用如下的二元組表示：

NegativeEvidence=

其中，Name表示負(fù)證據(jù)的名稱，RiskValue為負(fù)證據(jù)的風(fēng)險值，取值范圍為[1,10]，表示該負(fù)證據(jù)一旦被激活，所產(chǎn)生的負(fù)面影響，風(fēng)險值越大，其產(chǎn)生的負(fù)面影響越大.例如，表3列舉了三個風(fēng)險值不同的負(fù)證據(jù).

表3 負(fù)證據(jù)示例Tab.3 Examples of negative evidence

本文在標(biāo)準(zhǔn)[27]給出的航天型號軟件C語言安全子集和文獻(xiàn)[24]中提出的面向源代碼的軟件可信規(guī)范基礎(chǔ)上，建立面向源代碼的航天型號軟件C語言可信證據(jù)規(guī)范.該可信證據(jù)規(guī)范分為表達(dá)式類、聲明定義類、語句類、參數(shù)與注釋類等四類，共109個正可信證據(jù)，其中，正證據(jù)共57個，負(fù)證據(jù)共52個，關(guān)鍵證據(jù)36個，非關(guān)鍵證據(jù)73個，具體各類數(shù)目如表4所示.

表4 負(fù)證據(jù)示例Tab.4 Trustworthy evidence statistics

2 面向源代碼的航天軟件可信性度量模型

2.1 面向源代碼的航天軟件可信性度量模型框架

為了便于從源代碼角度對航天軟件可信性進(jìn)行度量，本文提出了一個面向C語言源代碼可信證據(jù)的航天軟件可信性度量模型框架.該框架如圖2所示，首先對源代碼進(jìn)行分析，結(jié)合證據(jù)集，找出其中存在的正證據(jù)和負(fù)證據(jù)；根據(jù)基于正證據(jù)類的航天軟件可信性度量模型和基于負(fù)證據(jù)類的航天軟件可信度度量模型分別計算基于每類證據(jù)的軟件可信值；然后根據(jù)基于混合證據(jù)的航天軟件可信性度量模型對得到的可信值進(jìn)行融合得到最終的軟件可信值；最后根據(jù)軟件可信性分級模型得到軟件的可信等級.

圖2 面向源代碼的航天軟件可信性度量模型框架Fig.2 Aerospace software trustworthiness measurement framework oriented to source code

2.2 基于正證據(jù)的航天軟件可信性度量模型

在面向源代碼的軟件可信性度量中，從源代碼出發(fā)得到正證據(jù)，這些正證據(jù)按照其特點劃分為多種類別，在本文中，我們將其劃分為4個類別，分別為表達(dá)式類、聲明定義類、語句類、參數(shù)與注釋類等4類.根據(jù)每類中每個關(guān)鍵正證據(jù)和其所占權(quán)重計算出關(guān)鍵正證據(jù)可信度量值，每個非關(guān)鍵正證據(jù)的度量值和其所占權(quán)重計算出非關(guān)鍵正證據(jù)的可信度量值，由此計算出這一類正證據(jù)的可信度量值，基于此本文給出如下基于正證據(jù)的航天軟件可信性度量模型.

假設(shè)正證據(jù)共有cp類，第p類正證據(jù)共有m個關(guān)鍵證據(jù)，s個非關(guān)鍵證據(jù)，則基于正證據(jù)類的航天軟件可信性度量模型計算公式為：

其中，α表示所有關(guān)鍵正證據(jù)在正證據(jù)中所占權(quán)重，β表示所有非關(guān)鍵正證據(jù)在正證據(jù)中所占權(quán)重，yi(1≤i≤m)為關(guān)鍵正證據(jù)可信度量值，yj(m+1≤j≤m+s)為非關(guān)鍵正證據(jù)可信度量值，αi為關(guān)鍵正證據(jù)ei在所有關(guān)鍵正證據(jù)中所占權(quán)重，βj為非關(guān)鍵正證據(jù)ej在所有非關(guān)鍵正證據(jù)中所占權(quán)重.

該模型符合文獻(xiàn)[24]中基于公理化方法所提出的非負(fù)性、比例合適性、單調(diào)性、凝聚性、靈敏性、替代性和可期望性7個度量屬性.該模型還符合“木桶原理”，即單個正證據(jù)的度量值較高，最終的度量值不一定很高，但是如果有一個正度量值很低，那么最終的度量值一定很低.

2.3 基于負(fù)證據(jù)的航天軟件可信性度量模型

負(fù)證據(jù)出現(xiàn)次數(shù)越多，軟件失效可能性就越大，軟件就越有可能向用戶預(yù)期之外的情況運(yùn)行，軟件可信性就越低.此外，如果源代碼中出現(xiàn)的負(fù)證據(jù)風(fēng)險值較高，該負(fù)證據(jù)被激活產(chǎn)生的影響就越大，軟件的可信性也就越低.因此，本文給出如下基于負(fù)證據(jù)的航天軟件可信性度量模型.

假設(shè)負(fù)證據(jù)共有cn類，第q類負(fù)證據(jù)集中共有l(wèi)條負(fù)證據(jù)，則此軟件在第q類負(fù)證據(jù)影響下的總風(fēng)險值為：

(2)

其中，ni為負(fù)證據(jù)ei在程序中出現(xiàn)的次數(shù)，RiskValuei為負(fù)證據(jù)ei風(fēng)險值.

軟件的風(fēng)險值表示軟件會向用戶預(yù)期之外運(yùn)行的風(fēng)險程度，軟件風(fēng)險值越大，軟件可信性就越小.文獻(xiàn)[28-29]中提出了一個基于失信證據(jù)的軟件可信性度量模型，本文在此基礎(chǔ)上，將軟件在該類負(fù)證據(jù)影響下的風(fēng)險值SRValue作為自變量，該類負(fù)證據(jù)的可信度量值TNq作為因變量，可得到基于負(fù)證據(jù)的航天軟件可信性度量模型計算公式為

(3)

其中，λ為參數(shù)，用來調(diào)節(jié)軟件風(fēng)險值對軟件可信性影響大小，一般選擇使用軟件行數(shù)來調(diào)節(jié)影響.

考慮到式(1)的取值范圍是[1,10],而式(3)的取值范圍是[0,1]，為了使得式(3)的取值范圍和式(1)一致，通過分段函數(shù)將軟件可信度的取值范圍映射到[1,10]，即

(4)

該模型綜合考慮了負(fù)證據(jù)的出現(xiàn)次數(shù)和其風(fēng)險程度，而且當(dāng)總風(fēng)險值較低的情況下，其可信度隨總風(fēng)險值下降幅度較大.反之，當(dāng)總風(fēng)險值較高的情況下，其可信度隨總風(fēng)險值下降幅度較小.

2.4 基于混合證據(jù)的航天軟件可信性度量模型

軟件可信性是由源代碼中所有可信證據(jù)共同決定的，僅通過某類正證據(jù)或者某類負(fù)證據(jù)來度量軟件可信性都會忽略源代碼中很多要素，因此軟件可信性度量要綜合考慮軟件中所有可信證據(jù).根據(jù)每類正證據(jù)和負(fù)證據(jù)所占的權(quán)重對正負(fù)證據(jù)所計算出的軟件可信值進(jìn)行融合，得到基于混合證據(jù)的軟件可信值，然后根據(jù)每類證據(jù)所占的權(quán)重對各個類的正負(fù)證據(jù)所計算出的軟件可信值進(jìn)行融合，得到基于混合證據(jù)的可信值.基于此，本文給出如下基于混合證據(jù)的航天軟件可信性度量模型.

(5)

其中，ωh為第h類證據(jù)所占權(quán)重，γ為參數(shù)，表示正證據(jù)和負(fù)證據(jù)對軟件可信度的不同影響.

該模型綜合考慮了正負(fù)證據(jù)的共同影響，而且在由各類證據(jù)可信度計算整體可信度時，計算公式同樣符合木桶原理.

3 軟件可信性分級模型

王靖等[30]在航天嵌入式軟件可信性評估時根據(jù)計算出的軟件整體可信值和各個屬性的可信值把軟件分為5個等級.在王婧等人的基礎(chǔ)上，結(jié)合之前所給出的計算模型和關(guān)鍵證據(jù)與非關(guān)鍵證據(jù)的定義，給出面向源代碼的軟件可信性分級模型，如表5所示，其中l(wèi)ine表示程序行數(shù).

表5 軟件可信性分級模型Tab.5 Software trustworthy classification model

該軟件可信性分級模型滿足以下性質(zhì)：

性質(zhì)1.門限性

門限性是指某一可信等級的軟件可信值必須要達(dá)到此等級所要求最低可信值，其所有正證據(jù)都要達(dá)到某一等級，出現(xiàn)負(fù)證據(jù)的風(fēng)險值不能超過最高要求的風(fēng)險值.該性質(zhì)表明要達(dá)到某一可信等級的軟件，除了其可信值需要達(dá)到要求以外，還需要滿足正證據(jù)的度量值不能太低，出現(xiàn)負(fù)證據(jù)的風(fēng)險值不能太高.因此，僅僅某一個正證據(jù)度量值或負(fù)證據(jù)風(fēng)險值改變不一定能提高軟件可信等級，還要提高可信值最低的正證據(jù)度量值和避免風(fēng)險值較高的負(fù)證據(jù)出現(xiàn).

性質(zhì)2.關(guān)鍵性

關(guān)鍵性是指某一可信等級的軟件需要滿足其關(guān)鍵證據(jù)的可信值或總風(fēng)險值要滿足一定的要求.由于不同類型的軟件關(guān)鍵證據(jù)和非關(guān)鍵證據(jù)不同，該性質(zhì)對于不同類型提出了不同要求.

4 實驗與分析

NASA作為美國國家航空航天局，負(fù)責(zé)規(guī)劃和實施美國國家航天計劃，并展開科學(xué)研究.自其成立以來，NASA實施了多項成功的太空計劃，其成功必然離不開其高可信軟件.本文選取了NASA在代碼開源托管平臺Github上開源的Core Flight Executive代碼(https:∥github.com/nasa/cFE)，它是Core Flight System的框架組件.本節(jié)將以該系統(tǒng)代碼的msg模塊為度量對象，驗證本文所提出的面向源代碼的航天軟件可信性度量方法的有效性與實用性.該模塊代碼行數(shù)1256行，包含11個文件，文件結(jié)構(gòu)如圖3所示.

圖3 文件結(jié)構(gòu)Fig.3 File structure

4.1 證據(jù)提取

本文已經(jīng)根據(jù)標(biāo)準(zhǔn)[27]和文獻(xiàn)[24]建立了面向航天嵌入式C語言代碼的可信證據(jù)規(guī)范，區(qū)分關(guān)鍵證據(jù)與非關(guān)鍵證據(jù)以及可信正證據(jù)與可信負(fù)證據(jù).

本文首先依照可信正證據(jù)對該源代碼進(jìn)行評估，得到各條正證據(jù)的評估結(jié)果，其結(jié)果如表6所示.其中表達(dá)式類共有13個證據(jù)被評為A，4個證據(jù)被評為B；聲明定義類共有10個證據(jù)被評為A，4個證據(jù)被評為B；語句類所有15個證據(jù)都被評為A；參數(shù)注釋類共有8個證據(jù)被評為A，2個證據(jù)被評為B.數(shù)組下標(biāo)越界關(guān)鍵證據(jù)評為B，其他為A.

表6 正證據(jù)度量結(jié)果Tab.6 Positive Evidence measurement results

然后根據(jù)可信負(fù)證據(jù)，在源代碼中判斷負(fù)證據(jù)的出現(xiàn)次數(shù)，結(jié)果如表7所示.其中，表達(dá)式類負(fù)證據(jù)沒有出現(xiàn)；聲明定義類負(fù)證據(jù)出現(xiàn)3次，總風(fēng)險值為15；語句類負(fù)證據(jù)出現(xiàn)17次，總風(fēng)險值為51；參數(shù)注釋類負(fù)證據(jù)沒有出現(xiàn)；沒有出現(xiàn)關(guān)鍵負(fù)證據(jù).

表7 負(fù)證據(jù)度量結(jié)果Tab.7 Negative Evidence measurement results

4.2 可信度計算

本小節(jié)通過4.1節(jié)中得到的證據(jù)度量結(jié)果和本文提出的度量方法對msg模塊進(jìn)行可信度計算.本文采用的參數(shù)和權(quán)重值如表8所示.

表8 參數(shù)和權(quán)重值表Table 8 Parameters and weight values

其中，為了便于計算，在正證據(jù)可信度計算中，由于關(guān)鍵證據(jù)每類均是5個，令關(guān)鍵正證據(jù)ei在所有關(guān)鍵證據(jù)中所占的權(quán)重αi均相等，因此αi的值均取1/5，令每類非關(guān)鍵正證據(jù)ej在每類所有非關(guān)鍵正證據(jù)中所占的權(quán)重βj均相等，因此，表達(dá)式類權(quán)重為1/12，聲明定義類權(quán)重為1/9，語句類權(quán)重為0.1，參數(shù)注釋類權(quán)重為0.2.每類正證據(jù)所占的權(quán)重均為1/4，每類負(fù)證據(jù)所占的權(quán)重均為1/4.

通過每個正證據(jù)的度量結(jié)果計算出的此類正證據(jù)的可信度量值為：

TP1=0.6×10+0.4×8.87=9.55,

TP2=0.6×9.31+0.4×8.53=9.00,

TP3=0.6×10+0.4×10=10.00,

TP4=0.6×10+0.4×8.67=9.47,

通過各類負(fù)證據(jù)計算的此類負(fù)證據(jù)的可信度量值為：

TN1=e0=1.000,

TN2=e-0.015=0.985,

TN3=e-0.051=0.950,

TN4=e0=1.000,

基于混合證據(jù)計算的軟件可信度為：

T1=9.550.5×10.000.5=9.77,

T2=9.000.5×9.850.5=9.42,

T3=10.000.5×9.500.5=9.75,

T4=9.470.5×10.000.5=9.73,

T=9.770.25×9.420.25×9.750.25×9.730.25=9.6

最終計算得出軟件的可信度為9.67，可信度量值大于9.5，但是關(guān)鍵正證據(jù)“數(shù)組下標(biāo)越界檢查”度量值為B，因此該軟件的可信等級為Ⅳ級.

Core Flight Executive作為NASA Core Flight System的核心軟件，在開源社區(qū)Github獲得較多好評，并且NASA在開源該代碼之前也使用其作為部分飛行器的代碼，因此其可信性較高，本文的可信量化評估結(jié)果符合該軟件的實際情況.

5 結(jié) 論

作為安全攸關(guān)的領(lǐng)域之一，航天軟件的可信性至關(guān)重要.通過有效的方法評估航天軟件可信性，并用形象易懂的方式體現(xiàn)出軟件的可信程度可以為提高軟件可信性和減少因軟件不可信而導(dǎo)致的災(zāi)難提供依據(jù)和參考.

本文首先建立了面向航天型號軟件的C語言可信證據(jù)規(guī)范，并提出了一種面向源代碼的航天軟件可信性度量方法，分別計算在每類可信正證據(jù)和可信負(fù)證據(jù)的可信度量值，然后使用基于混合證據(jù)的軟件可信度量模型計算最終的軟件可信度.在此基礎(chǔ)上，本文提出了一種面向航天領(lǐng)域的軟件可信分級模型，用來展現(xiàn)軟件的可信程度，并且使用NASA的開源軟件Core Flight Executive驗證了本文所提出的可信量化評估方法具有很好的有效性和實用性.