软件安全性需求形式化建模和验证

基本信息

• 商品名称：软件安全性需求形式化建模和验证
• 作者：李震|责编:吴昌兴
• 定价：42
• 出版社：江苏大学
• ISBN号：9787568401128

其他参考信息（以实物为准）

• 出版时间：2019-11-01
• 印刷时间：2019-11-01
• 版次：1
• 印次：1
• 开本：32开
• 包装：平装
• 页数：187
• 字数：162千字

内容提要

本书共分为7个章节。
     第1章：绪论。介绍背景和意义， 外在软件安 全性需求形式化建模和验证领域的相关研究现状；说 明本书的主要研究内容。
     第2章：基本概念和方法。相关的基本概念和方法 的介绍。
     第3章：软件安全性需求过程。介绍 外 的 软件安全性领域相关的 标准和手册，生成可操作 的软件安全性需求工作过程，并且将其划分为相应的 子过程。
     第4章：软件安全性需求形式化建模。按照本体的 “七步法”的建模步骤和合并规则，根据遴选的安全 性领域相关的 标准和手册，建立软件安全性需求 本体的概貌模型和相应的子过程模型。针对软件系统 模型的安全性和复杂性特征，提出了软件安全Petri网 模型——SEPN，并给出了SEPN的形式定义、迁移的使 能条件和引发运算规则。
     第5章：软件安全性需求形式化验证。从遴选的安 全性领域相关的 标准和手册中提取出软件安全性 需求的静态需求，利用本体模型中的概念和关联描述 静态验证所需的形式化验证规则。建立了扩展Petri网 和模型检验语言NuSMV的语义映射，设计并实现了SEPN 向NuSMV程序语言的转换算法，设计并实现了扩展 Petri网子模型自动划分和定级排序的递归算法。
     第6章：工具原型设计。简要介绍了软件安全性需 求建模和验证工具原型的设计和开发，包括功能概述 和设计概述。
     第7章：实验和实例。实验模拟3个复杂程度递增 的软件安全性功能作为需求静态分析和验证的对象， 选取4名安全性人员，分为形式化组和人工分析两个组 ，记录分析和验证的过程和时间、发现问题的数目， 修改确认和回归问题的次数和时间，对实验的结果进 行分析。选取机载除冰系统软件作为典型的安全关键 软件实例，对其进行系统的形式化建模和验证实例应 用。
     第8章：结论与展望。概括本书研究的内容，阐述 取得的成果，指出尚存在的问题，提出对未来工作的 展望。
    

目录

第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章 软件安全性需求形式化验证