第1章 绪论
1.1 研究工作的意义
1.2 国内外相关研究现状
1.2.1 软件安全性概况
1.2.2 软件安全性需求建模
1.2.3 软件安全性需求验证
1.2.4 自动化工具
1.2.5 小结
1.3 研究内容与创新
1.4 结构框架
1.5 本章小结
第2章 基本概念和方法
2.1 软件安全性
2.1.1 软件安全性定义
2.1.2 软件安全性需求定义
2.2 形式化方法
2.2.1 概述
2.2.2 本体
2.2.3 Petri网
2.2.4 模型检验
2.2.5 分析和说明
2.3 本章小结
第3章 软件安全性需求过程
3.1 标准和手册
3.2 过程概述
3.3 软件和系统安全性子过程
3.3.1 初步危险分析
3.3.2 识别安全关键软件
3.3.3 风险分级
3.4 软件安全性策划子过程
3.4.1 刻画安全关键软件
3.4.2 确定软件风险指数
3.4.3 确定安全性工作
3.5 软件需求子过程
3.5.1 通用安全性需求获取
3.5.2 特定安全性需求获取
3.5.3 需求关键性分析
3.6 本章小结
第4章 软件安全性需求形式化建模
4.1 基于本体的静态建模
4.1.1 本体建模
4.1.2 E-R模型概貌
4.1.3 软件和系统安全性阶段子模型
4.1.4 软件安全性策划阶段子模型
4.1.5 软件需求阶段子模型
4.2 基于Petri网的动态建模
4.2.1 基本Petri网
4.2.2 软件安全Petri网
4.3 本章小结
第5章 软件安全性需求形式化验证
5.1 静态验证
5.1.1 软件和系统安全性子阶段验证
5.1.2 软件安全性策划子阶段验证
5.1.3 软件需求子阶段验证
5.2 动态验证
5.2.1 模型检验
5.2.2 NuSMV
5.2.3 语义映射
5.2.4 代码自动生成
5.2.5 划分和定级
5.3 本章小结
第6章 工具原型设计
6.1 功能概述
6.2 设计概述
6.2.1 系统设计
6.2.2 表设计
6.2.3 查询设计
6.2.4 界面设计
6.3 本章小结
第7章 实验和实例
7.1 实验
7.1.1 实验概述
7.1.2 实验步骤
7.1.3 实验目的
7.1.4 实验人员
7.1.5 实验数据
7.1.6 实验结果
7.1.7 总结和讨论
7.2 实例
7.2.1 系统概述
7.2.2 形式化建模
7.2.3 形式化验证
7.3 本章小结
第8章 结论与展望
8.1 主要研究成果
8.2 未来工作展望
参考文献
附录A 实验软件需求
附录B 自动生成的NuSMV代码