[發(fā)明專利]一種基于形式化及統(tǒng)一軟件模型的軟件可信工程方法

無效

• 申請?zhí)枺?/td>: 201110046569.8
• 申請日: 2011-02-25
• 公開（公告）號: CN102136047A
• 公開（公告）日: 2011-07-27
• 發(fā)明（設計）人: 李曉紅;曹坤宇;陳世展;饒國政;邢金亮;曹燕
• 申請（專利權）人: 天津大學
• 主分類號: G06F21/00
• 分類號: G06F21/00;G06F11/36
• 代理公司: 天津市北洋有限責任專利代理事務所 12201
• 代理人: 溫國林

技術領域

本發(fā)明以可信軟件開發(fā)過程作為主要對象，搭建了結(jié)合形式化方法的軟件工程理論體系，改進了現(xiàn)有軟件工程非形式化的本質(zhì)不足，并引入缺陷檢測機制，在軟件設計階段檢測并緩和缺陷，屬于軟件可信領域，特別涉及一種基于形式化及統(tǒng)一軟件模型的軟件可信工程方法。

背景技術

隨著計算機應用的不斷發(fā)展，在信息社會中發(fā)揮著至關重要的作用。但是軟件的生產(chǎn)現(xiàn)狀不能令人滿意，軟件安全事故、軟件質(zhì)量問題和軟件擴展問題已經(jīng)帶來了巨大的損失。國內(nèi)外專家及行業(yè)巨頭已經(jīng)將軟件的可信性作為軟件的一個重要屬性。軟件系統(tǒng)的可信性質(zhì)，具體為軟件系統(tǒng)需要滿足的關鍵性質(zhì)，當軟件系統(tǒng)一旦違背這些關鍵性質(zhì)會造成不可容忍的損失時，稱這些關鍵性質(zhì)為高可信性質(zhì)。其中高可信性質(zhì)包括：可靠性(reliability)、可靠安全性(safety)、保密安全性(security)、生存性(survivability)、機密性(confidentiality)、完整性(integrity)和可維護性(maintainability)等。軟件的可信性問題自軟件開發(fā)以來久已存在。人們在軟件工程的實踐中從需求分析方法、設計和測試多個方面提出了一些方法來試圖從開發(fā)的角度獲得和評估軟件的這些性質(zhì)。例如，在需求分析中軟件安全性分析技術，在軟件設計中的軟件容錯技術，在軟件測試中的軟件可靠性測試技術。并且，國際上已經(jīng)開始將軟件過程模型與可信軟件開發(fā)聯(lián)系起來。例如，面向可靠性的凈室軟件工程法、面向安全性的軟件開發(fā)過程中錯誤發(fā)生機制與軟件性質(zhì)定量預測模型。

形式化方法是一種經(jīng)實踐證明的高質(zhì)量軟件的構建方法，構建可信軟件的一種公認的關鍵技術。形式化方法最主要的優(yōu)點為可以進行形式化推理和證明。形式化驗證就是在形式化規(guī)約的基礎上建立軟件系統(tǒng)及其性質(zhì)的關系，即分析系統(tǒng)是否具有所期望性質(zhì)的過程，主要分有兩種途徑：模型檢驗和定理證明。模型檢驗是通過搜索待驗證軟件系統(tǒng)模型的有窮狀態(tài)空間來檢驗系統(tǒng)的行為是否具備預期性質(zhì)的一種有窮狀態(tài)系統(tǒng)自動驗證技術。定理證明是將軟件系統(tǒng)和性質(zhì)都用邏輯方法來規(guī)約，通過基于公理和推理規(guī)則組成的形式系統(tǒng)，以如同數(shù)學中定理證明的方法來證明軟件系統(tǒng)是否具備所期望的關鍵性質(zhì)。基于定理證明的形式化驗證技術可以看作是以軟件系統(tǒng)為公理獲得其性質(zhì)的證明過程。

軟件安全性是軟件可信性的一個重要方面，軟件安全缺陷是軟件自身的一種內(nèi)在屬性，是安全問題的根源，被攻擊者惡意利用后形成軟件攻擊，造成巨大的損失。軟件的安全缺陷主要分成兩大類，包括軟件設計階段引入的缺陷和軟件實現(xiàn)階段引入的缺陷。在軟件開發(fā)生命周期中，設計階段安全缺陷的發(fā)現(xiàn)和修正非常重要，因為修改設計模型消耗的成本遠遠小于修改軟件成品消耗的成本。目前有大量的工具和方法致力于檢測和消除軟件實現(xiàn)階段的安全缺陷，但是，軟件設計階段安全缺陷檢測方法和工具卻并不成熟。因此，有必要對設計階段引入的安全缺陷進行分析和研究，包括缺陷的內(nèi)部機制，產(chǎn)生原因等，抽象軟件缺陷的本質(zhì)結(jié)構，進而基于此結(jié)構進行形式化建模，構建安全缺陷知識庫，使計算機能夠自動處理此類缺陷。

發(fā)明內(nèi)容

為了解決傳統(tǒng)軟件工程的不足，本發(fā)明提供了一種基于形式化及統(tǒng)一軟件模型的軟件可信工程方法，所述方法包括以下步驟：

(1)基于形式化語言、傳統(tǒng)UML視圖，構建包含軟件需求設計信息、軟件實現(xiàn)信息和運行環(huán)境信息的統(tǒng)一軟件模型；

(2)根據(jù)軟件可信工程技術架構，進行所述統(tǒng)一軟件模型的一致性和有效性驗證，并自動生成單元測試實例；

(3)構建基于所述統(tǒng)一軟件模型的軟件安全缺陷知識庫；

(4)基于所述軟件安全缺陷知識庫，通過定理證明機，發(fā)現(xiàn)所述統(tǒng)一軟件模型中潛在的軟件安全缺陷；并根據(jù)所述潛在的軟件安全缺陷給出相應的緩和方案。所述統(tǒng)一軟件模型包括：需求部分、設計部分和實現(xiàn)部分，

其中，所述需求部分由UML用例圖、活動圖和狀態(tài)圖組成，所述活動圖和所述狀態(tài)圖作為所述UML用例圖的補充，描述需求中的動態(tài)信息；所述設計部分由順序圖與形式化語言組成，以功能單元為最小單位，所述順序圖作為框架，描述了完成預設功能需要調(diào)用的相應功能單元及調(diào)用規(guī)則；所述形式化語言通過形式化的描述增加了功能單元的語義信息；所述實現(xiàn)部分由實現(xiàn)功能單元的程序設計語言代碼單元組成，且滿足所述形式化語言描述。