軟件保證舉證方法及其應用

曾福萍，女，北京航空航天大學講師，碩士生導師。碩士畢業後一直在北京航空航天大學可靠性工程研究所從事與軟件可靠性、軟件安全性、軟件測試相關的教學、科研、工程和管理工作，期間獲得了在職博士學位。主要研究方向為軟件可靠性設計、軟件安全性分析與評估、軟件測試、軟件代碼分析等技術的研究與應用。主持多項裝發共用技術和領域基金、省部級項目以及軍工項目，參與過裝發十一五、十二五、十三五、國防技術基礎、可靠性維修性保障性技術集成及在某導彈的應用驗證、一飛院安全性、空軍大飛機辦技術服務、軟件測試等二十余項項目。在國內外學術期刊上發表相關論文及專利幾十篇，獲國防技術進步一等獎二項。參與編寫《軟件可靠性工程》專著一部。目前是裝發可靠性專業組秘書，中國指揮與控制學會可靠性系統科學與工程專業委員會委員、紀檢委員，中國計算機學會軟件工程專業委員會委員。

目 錄

 

第1章 軟件保證舉證概述 1

1.1 軟件保證舉證的由來及意義 1

1.2 軟件保證舉證的研究現狀 3

1.3 軟件保證舉證的基本知識 5

1.3.1 軟件保證舉證的概念 5

1.3.2 軟件保證舉證的結構 5

1.3.3 軟件保證舉證的表述方法 9

1.4 GSN 12

1.4.1 GSN的基本符號 13

1.4.2 GSN的模式符號 22

1.4.3 GSN的模塊符號 26

1.4.4 GSN軟件保證舉證的構建流程 35

1.4.5 GSN軟件保證舉證的構建工具 49

本章小結 51

參考文獻 52

第2章 軟件安全性舉證方法 53

2.1 軟件安全性舉證的基礎知識 53

2.1.1 軟件安全性的概念 53

2.1.2 軟件安全性舉證的概念 59

2.2 軟件安全性舉證框架的構建原理 60

2.3 軟件安全性舉證框架 63

2.3.1 軟件安全性過程因素包 65

2.3.2 軟件安全性需求分析包 68

2.3.3 危險軟件失效分析包 73

2.3.4 危險軟件失效的消除或緩解實現包 75

2.3.5 危險軟件失效的消除或緩解驗證包 76

2.3.6 軟件安全性證據包 76

2.4 基於GSN的軟件安全性舉證的論證模式 77

2.4.1 系統級別的安全性的論證模式 77

2.4.2 軟件對系統危險貢獻的緩解的論證模式 80

2.4.3 軟件安全性頂層的論證模式 81

2.4.4 軟件安全性需求實現的論證模式 84

2.4.5 危險軟件失效已被消除或緩解的論證模式 85

2.4.6 軟件失效改進措施實現的論證模式 87

2.5 應用實例 89

2.5.1 剎車系統介紹 89

2.5.2 應用過程 90

2.5.3 應用結果 90

本章小結 101

參考文獻 101

第3章 軟件可靠性舉證方法 102

3.1 軟件可靠性舉證的基礎知識 102

3.1.1 幾個基本概念 102

3.1.2 軟件可靠性工程 104

3.1.3 軟件可靠性相關標準 105

3.2 軟件可靠性舉證框架 106

3.2.1 基於軟件可靠性特性度量模型的軟件可靠性舉證框架 107

3.2.2 基於缺陷防控模型的軟件可靠性舉證框架 111

3.2.3 基於“4+1”準則的軟件可靠性舉證框架 113

3.2.4 幾種框架的分析比較 117

3.3 基於GSN的軟件可靠性舉證的論證模式 118

3.3.1 基於軟件可靠性特性度量模型的軟件可靠性舉證的論證

模式 118

3.3.2 基於缺陷防控模型的軟件可靠性舉證的論證模式 121

3.3.3 基於"4+1"準則的軟件可靠性舉證的論證模式 123

3.4 應用實例 127

3.4.1 實例軟件簡介 128

3.4.2 基於軟件可靠性特性度量模型的軟件可靠性舉證的應用過程 129

3.4.3 基於缺陷防控模型的軟件可靠性舉證的應用過程 130

3.4.4 基於“4+1”準則的軟件可靠性舉證的應用過程 134

本章小結 140

參考文獻 141

第4章 軟件保密性舉證方法 142

4.1 軟件保密性舉證的基礎知識 143

4.1.1 軟件保密性的相關概念 143

4.1.2 軟件保密性舉證的概念 146

4.2 軟件保密性舉證框架及基於GSN的軟件保密性舉證的論證模式 148

4.2.1 軟件保密性舉證框架的結構 148

4.2.2 軟件保密性舉證框架的基本論證原理 149

4.2.3 軟件保密性舉證框架的論證結構 159

4.2.4 軟件保密性舉證框架的實例化方法 187

4.3 應用實例 189

本章小結 199

參考文獻 199

第5章 軟件可信性舉證方法 201

5.1 軟件可信性舉證的基礎知識 201

5.1.1 軟件可信性的相關概念 201

5.1.2 軟件可信性舉證的相關研究 205

5.2 基於GSN的軟件可信性舉證框架及論證模式 206

5.2.1 基於GSN的軟件可信性舉證框架 206

5.2.2 基於GSN的軟件可信性舉證的論證模式 208

5.2.3 軟件可信性舉證框架的實例化規則 235

5.3 應用實例 237

5.3.1 實例軟件簡介 237

5.3.2 舉證實例構建方案 237

5.3.3 舉證實例構建過程 239

本章小結 242

參考文獻 242

第6章 基於非形式邏輯理論的軟件保證舉證信心評定方法 244

6.1 軟件保證舉證信心評定方法的理論基礎 244

6.1.1 非形式邏輯 245

6.1.2 圖爾敏論證模型的論證評價 247

6.1.3 貝葉斯網絡 250

6.2 軟件保證舉證信心評定方法 251

6.2.1 保證舉證樹形結構到圖爾敏論證模型的轉化 252

6.2.2 圖爾敏論證模型的軟件保證舉證定性評價 256

6.2.3 圖爾敏論證模型的軟件保證舉證定量評價 258

6.3 應用實例 269

6.3.1 應用過程 271

6.3.2 應用分析 278

本章小結 279

參考文獻 279