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

曾福萍，女，北京航空航天大学讲师，硕士生导师。硕士毕业后一直在北京航空航天大学可靠性工程研究所从事与软件可靠性、软件安全性、软件测试相关的教学、科研、工程和管理工作，期间获得了在职博士学位。主要研究方向为软件可靠性设计、软件安全性分析与评估、软件测试、软件代码分析等技术的研究与应用。主持多项装发共用技术和领域基金、省部级项目以及军工项目，参与过装发十一五、十二五、十三五、国防技术基础、可靠性维修性保障性技术集成及在某导弹的应用验证、一飞院安全性、空军大飞机办技术服务、软件测试等二十余项项目。在国内外学术期刊上发表相关论文及专利几十篇，获国防技术进步一等奖二项。参与编写《软件可靠性工程》专著一部。目前是装发可靠性专业组秘书，中国指挥与控制学会可靠性系统科学与工程专业委员会委员、纪检委员，中国计算机学会软件工程专业委员会委员。

目 錄

第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