[發(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 | 代理人: | 溫國林 |
| 地址: | 300072*** | 國省代碼: | 天津;12 |
| 權(quán)利要求書: | 查看更多 | 說明書: | 查看更多 |
| 摘要: | |||
| 搜索關(guān)鍵詞: | 一種 基于 形式化 統(tǒng)一 軟件 模型 可信 工程 方法 | ||
技術(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ì)語言代碼單元組成,且滿足所述形式化語言描述。
該專利技術(shù)資料僅供研究查看技術(shù)是否侵權(quán)等信息,商用須獲得專利權(quán)人授權(quán)。該專利全部權(quán)利屬于天津大學(xué),未經(jīng)天津大學(xué)許可,擅自商用是侵權(quán)行為。如果您想購買此專利、獲得商業(yè)授權(quán)和技術(shù)合作,請聯(lián)系【客服】
本文鏈接:http://www.szxzyx.cn/pat/books/201110046569.8/2.html,轉(zhuǎn)載請聲明來源鉆瓜專利網(wǎng)。
- 同類專利
- 專利分類
G06F 電數(shù)字?jǐn)?shù)據(jù)處理
G06F21-00 防止未授權(quán)行為的保護(hù)計(jì)算機(jī)或計(jì)算機(jī)系統(tǒng)的安全裝置
G06F21-02 .通過保護(hù)計(jì)算機(jī)的特定內(nèi)部部件
G06F21-04 .通過保護(hù)特定的外圍設(shè)備,如鍵盤或顯示器
G06F21-06 .通過感知越權(quán)操作或外圍侵?jǐn)_
G06F21-20 .通過限制訪問計(jì)算機(jī)系統(tǒng)或計(jì)算機(jī)網(wǎng)絡(luò)中的節(jié)點(diǎn)
G06F21-22 .通過限制訪問或處理程序或過程
- 一種基于應(yīng)用軟件散布的軟件授權(quán)與保護(hù)方法及系統(tǒng)
- 一種用于航空機(jī)載設(shè)備的軟件在線加載系統(tǒng)及方法
- 軟件構(gòu)建方法、軟件構(gòu)建裝置和軟件構(gòu)建系統(tǒng)
- 惡意軟件檢測方法及裝置
- 一種基于軟件基因的軟件同源性分析方法和裝置
- 軟件引入系統(tǒng)、軟件引入方法及存儲介質(zhì)
- 軟件驗(yàn)證裝置、軟件驗(yàn)證方法以及軟件驗(yàn)證程序
- 使用靜態(tài)和動(dòng)態(tài)惡意軟件分析來擴(kuò)展惡意軟件的動(dòng)態(tài)檢測
- 一種工業(yè)控制軟件構(gòu)建方法和軟件構(gòu)建系統(tǒng)
- 可替換游戲軟件與測驗(yàn)軟件的裝置與方法





