俞烈彬，王立杰

(江蘇自動化研究所，江蘇 連云港 222061)

現(xiàn)代裝備中大部分電子設(shè)備的關(guān)鍵功能由軟件來完成，隨著系統(tǒng)自動化、智能化水平的不斷提高，軟件規(guī)模和復雜度也不斷提高，比如在F-22戰(zhàn)機的綜合航電系統(tǒng)中，軟件實現(xiàn)的航電功能高達80%，軟件代碼達到170萬余行。而在F-35戰(zhàn)機的先進綜合航電系統(tǒng)中，軟件代碼達到500萬～800萬行。這表明，越來越多的安全性關(guān)鍵系統(tǒng)軟件日益密集化。另一方面，由軟件引發(fā)的事故或事件卻頻發(fā)不斷:如2004年12月20日，一架F-22因飛行控制軟件故障而墜毀;2007年2月11日，12架F-22在穿越國際日期變更線時又因軟件缺陷問題造成導航故障，戰(zhàn)機被迫在無導航和通信能力下危險返航。由此可見，武器裝備中的軟件是否具備包括可靠、可用、安全等特性在內(nèi)的可信特征已成為衡量和影響武器裝備效能的最重要的指標，構(gòu)建可信的裝備軟件，對搶占未來信息化戰(zhàn)爭制高點有著重要的作用。

近十年來軟件的可信性研究一直受到廣泛重視。美國政府的“網(wǎng)絡(luò)與信息技術(shù)研究發(fā)展計劃(NITRD)”［1］中，列出了8個重點領(lǐng)域，有4個與“可信軟件”密切相關(guān)。美國自然科學基金會(NSF)在加州大學伯克利分校建立了科學與技術(shù)研究中心TRUST［2］，其研究內(nèi)容圍繞可信系統(tǒng)的設(shè)計、構(gòu)建和運行展開。國家自然科學基金的“可信軟件基礎(chǔ)研究”重大研究計劃［3］是目前國內(nèi)可信軟件研究的主要研究計劃之一，其重點支持對嵌入式軟件和網(wǎng)絡(luò)應(yīng)用軟件領(lǐng)域的軟件可信性進行研究。

1 可信軟件相關(guān)技術(shù)研究現(xiàn)狀

如果一個軟件系統(tǒng)的行為總是與用戶預(yù)期的行為和結(jié)果相一致，在受到干擾時仍能提供連續(xù)的服務(wù)，則稱該軟件可信［4］。目前可信軟件的研究方向主要集中在軟件可信性度量與評估、可信軟件的構(gòu)造與驗證、可信軟件的演化與控制等。

1.1 軟件可信性度量與評估

軟件的可信性是軟件提供服務(wù)時符合用戶期望的能力，不僅涵蓋了軟件質(zhì)量特性中功能性、可靠性、易用性、效率、可維護性和可移植性等，還應(yīng)包括安全性、實時性、可生存性等其他特性。國外研究可信軟件比較有成效的是德國達姆施塔特大學的Databases and Distributed Systems Group 的“可信計劃”［5］，該計劃的目標是解決可信分布式系統(tǒng)的若干問題。他們的結(jié)論是可信是一個綜合的性質(zhì)，包含以下特征:端到端安全，可用性，可靠性，時效性，一致性，可預(yù)測性，可擴展性等。可信組織Trustie制定的可信規(guī)范中定義軟件可信屬性包括［6］:可用性(Availability)，可靠性(Reliability)，安全性(Security)，實時性(Real Time)，可維護性(Maintainability)和可生存性(Survivability)。上述每個特性又由若干子特性構(gòu)成，這些屬性構(gòu)成了軟件可信屬性模型，如圖1所示。

圖1 軟件可信屬性

軟件可信評估是通過分級的方式對用戶的主觀感受進行評價，用戶根據(jù)證據(jù)描述軟件對某種可信屬性的滿足程度。一種可信屬性可能通過多個可信證據(jù)從不同的角度反映出來。一個軟件所有可信證據(jù)的集合以某種結(jié)構(gòu)進行組織后，就構(gòu)成了軟件可信證據(jù)模型。Trustie組織在文獻［6］中提出了一種證據(jù)模型，將可信證據(jù)分為開發(fā)階段證據(jù)、提交階段證據(jù)和應(yīng)用階段證據(jù)三個部分，如圖2所示。

圖2 軟件證據(jù)分類

軟件可信評估是對軟件可信屬性的綜合分析評估，是一個多屬性決策分析［7］(MADA，Multiple Attribute Decision Analysis)問題。軟件評估過程如圖3所示。針對MADA問題，傳統(tǒng)的方法有字典序法、簡單加性加權(quán)法、層次分析法［8］等。數(shù)學評估模型通過模糊理論將定性指標定量化，很好地解決了現(xiàn)有評估模型中指標單一、原始信息模糊的評估問題。由于屬性權(quán)重和偏好等決策要素的不確定性，近年來，研究熱點逐漸轉(zhuǎn)向?qū)δ：鄬傩詻Q策問題［9］(FMADM，F(xiàn)uzzy Multattribute Decision Making)的研究。

圖3 軟件可信評估過程

1.2 可信軟件的構(gòu)造與驗證

可信軟件構(gòu)造主要分為工程化方法和形式化方法。工程化方法的核心思想是建立嚴格的工程規(guī)范，在軟件生命周期內(nèi)的各個階段，通過規(guī)范管理和輔助工具，最大限度地減少人為錯誤的機會，或盡可能早地發(fā)現(xiàn)人為錯誤。但隨著對軟件可信性要求的提高，工程化方法漸漸不能滿足高可信軟件開發(fā)的要求。統(tǒng)計表明，傳統(tǒng)的非形式化的軟件工程技術(shù)對軟件質(zhì)量的保證具有一個難以逾越的鴻溝，而形式化方法是提高軟件質(zhì)量的重要途徑。形式化方法的研究分為兩類:一類是直接為以UML為代表的面向?qū)ο笳Z言增加形式化語義，如英國的pUML組(precise UML group)就致力于運用數(shù)學知識將UML發(fā)展為一種具備精確數(shù)學語義的描述語言;另一類是通過模型轉(zhuǎn)換得到模型對應(yīng)的形式化語言描述。目前常用的形式化語言工具有自動機、進程代數(shù)、Petri網(wǎng)、邏輯學等。形式化方法研究早期，研究者一般都是手動給出系統(tǒng)形式化描述。模型驅(qū)動架構(gòu)(MDA)［10］提出以后，基于模型驅(qū)動的可信軟件構(gòu)造與驗證迅速成為一個研究熱點，模型驅(qū)動方法可以很好地支持形式化的描述和說明，可以較為方便對軟件可信需求進行抽象建模，給出形式化的歸約，進行模型轉(zhuǎn)換、邏輯推理。模型驅(qū)動的形式化方法如圖4所示。澳大利亞昆士蘭大學的Soon-Kyeong Kim等［11］采用MDA方法，通過模型轉(zhuǎn)換集成形式化建模語言(Object-Z)與非形式化建模語言(UML)，對于集成Object-Z和UML的建模語言，使用可重用的MDA轉(zhuǎn)換框架。A.MEKKI［12］在MDA框架下完成了時間限定系統(tǒng)模型到時間自動機的自動轉(zhuǎn)換。

圖4 模型驅(qū)動的形式化方法

對于軟件的可信驗證，在傳統(tǒng)軟件工程中，主要通過軟件可靠性測試來實現(xiàn)。在高可信軟件工程領(lǐng)域，常采用形式化的驗證方法。形式化驗證的主要技術(shù)有模型檢驗和定理證明。模型檢驗技術(shù)［13］是通過搜索待驗證軟件系統(tǒng)模型的有窮狀態(tài)空間來檢驗系統(tǒng)的行為是否具備預(yù)期性質(zhì)的一種有窮狀態(tài)系統(tǒng)自動驗證技術(shù)，其過程如圖5所示。RWTH Aachen University的Schlich B提出了一種基于嵌入式軟件匯編碼的模型檢驗方法［14］，該方法結(jié)合了模型檢驗、靜態(tài)分析和抽象解釋等手段，同時使用一個定制的模擬器建立了狀態(tài)矢量空間來控制不確定性。隨著國內(nèi)外對模型檢驗技術(shù)的深入研究，為了驗證系統(tǒng)以及系統(tǒng)性質(zhì)，出現(xiàn)了SPIN、DESIGN/CPN、UPPAAL等模型檢驗工具。

圖5 模型檢驗過程

模型檢驗過程與模型檢驗技術(shù)不同，定理證明方法可以直接處理無限的狀態(tài)空間。定理證明技術(shù)將軟件系統(tǒng)和性質(zhì)用邏輯方法來規(guī)約，通過基于公理和推理規(guī)則組成的形式系統(tǒng)，以類似數(shù)學中定理證明的方法來證明軟件系統(tǒng)是否具備所期望的關(guān)鍵性質(zhì)［15］。明尼蘇達大學軟件學院數(shù)字科技中心針對引導規(guī)則被劃分為同步階段和異步階段的一階規(guī)約與聯(lián)合規(guī)約邏輯定義，提出了一種集中證明系統(tǒng)［16］，集中證明方法中定理證據(jù)搜索被集中在一個交叉的、可計算的區(qū)間內(nèi)，而且更具有一般推導性。我國在幾何定理及其證明方面處于國際領(lǐng)先地位，吳文俊院士提出數(shù)學機械化證明方法推動了定理機器證明的研究［17］，通過該方法可在微機上很快地證明困難的幾何定理。但目前定理證明方法的效率還較低，很難用于大系統(tǒng)的驗證。

1.3 可信軟件的演化與控制

軟件的動態(tài)演化是指軟件系統(tǒng)投入運行后，隨環(huán)境和需求變化而進行的變更［18］。在開放環(huán)境下，隨著軟件多變性的發(fā)展，新技術(shù)與新功能的演變越來越復雜，因此必須對軟件的動態(tài)行為進行監(jiān)控，形成對軟件動態(tài)演化中的可信性控制方法。軟件行為監(jiān)控和控制的基本框架如圖6所示。

圖6 軟件行為監(jiān)控和控制框架

目前研究者一般采用形式化方法進行軟件行為描述，如Petri網(wǎng)、自動機和進程代數(shù)等。得到系統(tǒng)行為描述后，一般需要進行形式化驗證。軟件行為監(jiān)控是行為可信評估的基礎(chǔ)，為了對軟件行為進行全面、準確、實時的監(jiān)控，很多研究者提出了相應(yīng)的軟件監(jiān)控方法。Diakov［19］等人提出了一種基于CORBA中間件平臺的軟件行為監(jiān)控框架，能自動生成監(jiān)測代碼來監(jiān)測構(gòu)件之間的交互行為。Li Jun［20］提出了一個軟件行為監(jiān)測框架，基于全局因果跟蹤技術(shù)捕獲多維軟件系統(tǒng)行為。Chen Feng［21］等人提出了一種運行時行為監(jiān)測框架MOP，該框架能根據(jù)給定的行為規(guī)約自動生成監(jiān)測器，動態(tài)監(jiān)測系統(tǒng)運行行為，一旦發(fā)現(xiàn)違約行為，能立即觸發(fā)用戶定義的操作進行容錯處理。為了提高軟件的持續(xù)可用性和軟件行為的可信性，有必要對軟件行為進行控制，其主要包括異常行為控制和演化行為控制。Garlan［22］等人研究了基于運行時體系結(jié)構(gòu)的自適應(yīng)系統(tǒng)Rainbow。它采用外置運行時體系結(jié)構(gòu)，通過Probe-Gauge-Consumer三層監(jiān)控機制，獲取和度量系統(tǒng)變化來觸發(fā)自適應(yīng)規(guī)則實現(xiàn)自適應(yīng)演化。文獻［23］也提出了一種面向體系結(jié)構(gòu)的自適應(yīng)系統(tǒng)Artennis-ARC。它采用內(nèi)置運行時體系結(jié)構(gòu)，通過Agent-Gauge-Monitor三層監(jiān)控機制，驅(qū)動軟件系統(tǒng)進行自適應(yīng)演化。

2 可信軟件技術(shù)面臨的挑戰(zhàn)

現(xiàn)代裝備軟件大部分是以嵌入式軟件的形式存在。嵌入式軟件具有高復雜性的特點，同時對以實時性、可生存性、安全性為代表的高可信特征具有迫切需求，這些都對傳統(tǒng)的軟件可信技術(shù)提出了挑戰(zhàn)。目前研究可信裝備軟件技術(shù)中存在的問題主要為以下三個方面。

1)可信性度量和評估:目前裝備軟件沒有形成完整統(tǒng)一的可信指標體系，缺乏軟件評估技術(shù)標準或規(guī)范;可信屬性單獨進行度量評估，沒有形成正確性、可靠性、安全性等屬性的綜合度量空間。

2)可信軟件構(gòu)造與驗證:模型驅(qū)動技術(shù)為可信軟件構(gòu)造提供了一個極好的基礎(chǔ)架構(gòu)，但是針對現(xiàn)代國防武器領(lǐng)域中復雜嵌入式軟件系統(tǒng)的高可信需求，目前已有的模型驅(qū)動相關(guān)技術(shù)中并沒有提供有效的模型精化、轉(zhuǎn)換以及生成可信代碼的有效方法，以及全過程連接方法;缺少異構(gòu)模型語義保持和一致性理論和方法;缺少裝備軟件可信構(gòu)造與驗證的系統(tǒng)方法，缺少可信軟件開發(fā)工具和支撐平臺;模型檢驗應(yīng)用面臨的主要挑戰(zhàn)是狀態(tài)爆炸問題，必須設(shè)計可以處理大型搜索空間的算法和數(shù)據(jù)結(jié)構(gòu)，因此這方面的研究主要針對模型抽象技術(shù)和系統(tǒng)狀態(tài)空間的存儲和搜索技術(shù)［24］。

3)傳統(tǒng)軟件監(jiān)控需求表達能力不強，監(jiān)控代碼分散。沒有形成開放和復雜環(huán)境下的可信軟件運行監(jiān)控模型和體系結(jié)構(gòu);缺乏可信軟件演化的保障機制;在行為描述方面，需要建立軟件可信性與軟件行為之間的內(nèi)在聯(lián)系和嚴格描述;在行為監(jiān)測方面，需要設(shè)計有效的收集可信性相關(guān)數(shù)據(jù)的行為監(jiān)測機制;在行為可信管理方面，需要研究基于行為監(jiān)測的可信評估方法，構(gòu)建基于行為監(jiān)測的可信管理框架;在行為控制方面，需要研究支持行為可信的軟件動態(tài)演化機制。

3 結(jié)束語

高可信軟件技術(shù)已成為國防信息技術(shù)及武器裝備中嵌入式軟件研發(fā)與應(yīng)用過程中最為關(guān)鍵的核心技術(shù)。目前國內(nèi)非常缺乏這方面的基礎(chǔ)理論、實現(xiàn)技術(shù)以及工具的研究。我國可信軟件的標準大多參考國外標準，整體落后于發(fā)達國家水平，從長遠發(fā)展來看，不利于我國國防基礎(chǔ)技術(shù)研究能力的提高和創(chuàng)新能力的培養(yǎng)。因此，為了適應(yīng)武器裝備的快速發(fā)展，加強和提高我國在國防領(lǐng)域中高可信裝備軟件的基礎(chǔ)技術(shù)研究能力和創(chuàng)新能力，提高軍工高精尖裝備產(chǎn)品的質(zhì)量，需要展開高可信相關(guān)技術(shù)的研究，構(gòu)建擁有自主知識產(chǎn)權(quán)的裝備軟件可信平臺，這對于減少因軟件缺陷帶來的巨大損失與生命傷害，以及有效保障和提升我國國防武器裝備的作戰(zhàn)效能具有極其重要的意義。

［1］網(wǎng)絡(luò)與信息技術(shù)研究發(fā)展計劃(NITRD).http:∥www.nitrd.gov

［2］TURST.http:∥www.truststc.org/

［3］劉克，單志廣，王戟，等.可信軟件基礎(chǔ)研究重大研究計劃綜述［J］.中國科學基金，2008，22(3):145-151.

［4］WANG Huai min，LIU Xu dong.etc.Software trustworthiness classification specification(TRUSTIE STCV2.0)［EB/OL］，2009.

［5］T.Anderson，A.Avizienis，W.Carter，et al.Dependability:basic concepts and terminology［J］.Series:Dependable Computing and Fault-Tolerant Systems，1994，5

［6］Trustie Group.A trustworthy software production environment for large scale software resource sharing and cooperativedevelopment［EB/OL］.2008:http:∥ www.trustie.org.

［7］J.B.Yang，Y.M.Wang，D.L.Xu，et al.The evidential reasoning approach for MADA under both probabilistic and fuzzy uncertainties［J］.European Journal of Operational Research，2006，171(1):309-343.

［8］J.B.Yang，J.Liu，J.Wang，et al.Belief rule-base inference methodology using the evidential reasoning approach-RIMER［J］.Systems，Man and Cybernetics，Part A:Systems and Humans，IEEE Transactions on，2006，36(2):266-285.

［9］姚爽，郭亞軍，黃瑋強.基于證據(jù)距離的改進 DS/AHP多屬性群決策方法［J］.控制與決策，2010，25(6):894-898.

［10］OMG MDA Guide Version 1.0.1.http:∥www.omg.org/cgi-bin/doc?omg/03-06-01，retrieved at 2009.

［11］Soon-Kyeong Kim，Damian Burger，David Carrington.An MDA Approach towards Integrating Formal and Informal Modeling Languages［J］.Formal Method，2005，LNCS P:448-464.

［12］A.MEKKI，M.GHAZEL.Time-constrained Systems Validation Using Mdamodel Transformation.A Railway Case Study.8th International Conference of Modeling and Simulation.May，2010:10-12.

［13］E.Clarke，K.Mcmillan，S.Campos，et al.Symbolic Model Checking［A］;Proceedings of the LNCS 1102［C］，1996.Springer:419-422.

［14］Schlich B.Model Checking of Software for Microcontrollers［J］.ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS，2010，9(4).

［15］COOK S A.The Complexity of Theorem-Proving Procedures［A］;Proc.3rdAnnu.ACM sympos.On Theory of Computing(NewYork)，assoc.Comput，1971:151-158.

［16］David Baelde，Dale Miller，Zachary Snow.Focused Inductive Theorem Proving［J］.Lecture Notes in Computer Science，2010，6173:278-292.

［17］吳文俊.初等幾何判定問題與機械化證明［J］.中國科學，1977(7):507-516.

［18］萬燦軍等.動態(tài)演化環(huán)境中可信軟件行為監(jiān)控研究與進展.計算機應(yīng)用研究.2009，26(4):1201-1204.

［19］DIAKOVK.etc.Monitoring of Distributed Component Interactions.Proc of IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing.NewYork，2000:229-243.

［20］LI Jun.Monitoring and Characterization of Componentbased Systems with Global Causality Capture［C］.Proc of the 23rd International Conference on Distributed Computing System，2003:422-431.

［21］CHEN Feng.etc.MOP:An Efficient and Generic Run Time Verification Framework. Proc of OOPSLA2007，2007:569-588.

［22］GARLAN D.etc.Rain-bow:Architecture-based Self-adaptation with Reusable Infrastructure.IEEE Computer，2004，37(10):46-54.

［23］徐鋒，呂建，鄭瑋.一個軟件服務(wù)協(xié)同中信任評估模型的設(shè)計［J］.軟件學報，2003，14(6):1043-1051.

［24］薛克.基于SPIN的UML活動圖驗證［D］.華東師范大學，2008.