[發明專利]一種基于形式化及統一軟件模型的軟件可信工程方法

無效

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

1.一種基于形式化及統一軟件模型的軟件可信工程方法，其特征在于，所述方法包括以下步驟：

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

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

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

(4)基于所述軟件安全缺陷知識庫，通過定理證明機，發現所述統一軟件模型中潛在的軟件安全缺陷；并根據所述潛在的軟件安全缺陷給出相應的緩和方案。

2.根據權利要求1所述的一種基于形式化及統一軟件模型的軟件可信工程方法，其特征在于，所述統一軟件模型包括：需求部分、設計部分和實現部分，

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

3.根據權利要求1所述的一種基于形式化及統一軟件模型的軟件可信工程方法，其特征在于，所述軟件可信工程技術架構包括：所述統一軟件模型、模型驗證模塊、單元測試模塊、缺陷檢測模塊、安全知識學習模塊、軟件可信評估模塊和軟件安全知識庫，

其中，所述統一軟件模型貫穿于可信軟件生命周期的各個階段，為其他模塊提供了不同層面的形式化語義信息；所述模型驗證模塊針對所述統一軟件模型中的所述順序圖與所述形式化語言，對軟件設計進行一致性、有效性驗證；所述單元測試模塊通過功能單元的形式化語言自動生成所述單元測試用例；所述缺陷檢測模塊使用所述軟件安全知識庫中存儲的形式化缺陷信息，查找設計階段的安全缺陷；所述安全知識學習模塊從外界半自動學習安全知識，更新所述軟件安全知識庫；所述軟件可信評估模塊量化評估軟件的可信度。

4.根據權利要求1所述的一種基于形式化及統一軟件模型的軟件可信工程方法，其特征在于，步驟(3)中的所述構建基于統一軟件模型的軟件安全缺陷知識庫具體包括：

根據CWE中的安全缺陷進行安全缺陷分析，抽象軟件安全缺陷基本結構；

對所述軟件安全缺陷基本結構進行形式化建模，構建安全缺陷形式化模型；

根據所述安全缺陷形式化模型，構建所述軟件安全缺陷知識庫。