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

無效

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

技術(shù)領(lǐng)域

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

背景技術(shù)

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

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

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

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

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

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

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

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

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

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