图书介绍
面向对象软件的形式验证技术pdf电子书版本下载
- 文志诚著 著
- 出版社： 上海：上海大学出版社
- ISBN：9787811186482
- 出版时间：2011
- 标注页数：172页
- 文件大小：17MB
- 文件页数：187页
- 主题词：博士－学位论文－汇编－上海市－2007
PDF下载
下载说明
面向对象软件的形式验证技术PDF格式电子书版下载
下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如 BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！
（文件页数 要大于 标注页数，上中下等多册电子书除外）
注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具
图书目录
第一章 前言 1
1.1 软件需求 1
1.2 需求规格说明 2
1.3 形式方法 3
1.4 形式规格说明 6
1.5 形式验证 7
1.6 定理证明技术 9
1.7 论文的主要研究内容 9
第二章 形式规格说明语言Object-Z 12
2.1 语法 12
2.2 语义 13
2.3 形式验证方法 14
2.3.1 初始状态存在性验证 15
2.3.2 推理类中的性质 15
2.4 实例：电梯操作系统 16
2.4.1 描述 16
2.4.2 形式验证 22
2.5 小结 25
第三章 产生证明责任验证Object-Z规格说明 27
3.1 产生证明责任 27
3.1.1 证明责任 28
3.1.2 从基类中产生证明责任 29
3.1.3 检查函数与操作符 32
3.1.4 在继承下产生证明责任 34
3.1.5 对象作为一个属性 42
3.1.6 对相关的性质产生证明责任 44
3.2 用Z/EVES验证证明责任 45
3.2.1 证明器Z/EVES 45
3.2.2 编辑 45
3.2.3 分析 47
3.2.4 验证 47
3.3 小结 49
第四章 Object-Z的多态性推理 50
4.1 Object-Z多态性 50
4.2 多态性推理规则 51
4.3 推理的重用 53
4.3.1 子类不变式与超类不变式相同 53
4.3.2 子类不变式对超类不变式加强但不扩充 55
4.3.3 子类不变式扩充但不加强 55
4.3.4 子类不变式既加强又扩充 56
4.4 实例研究 56
4.4.1 对于O.Join 58
4.4.2 对于O.Leave 60
4.5 小结 61
第五章 行为子类型验证方法 62
5.1 行为子类型定义 62
5.2 实现Object-Z行为子类型继承 64
5.2.1 不变式规则 65
5.2.2 操作规则 66
5.3 实例研究 67
5.4 验证行为子类型规格说明 70
5.4.1 对于不变式规则 70
5.4.2 对于操作规则 71
5.4.3 使用Z/EVES证明 77
5.5 小结 77
第六章 基于Object-Z的实时验证方法 79
6.1 实时部分与功能部分分离方法 79
6.1.1 时间变量定义 80
6.1.2 语法 81
6.1.3 操作完成的时间 84
6.1.4 实例研究 84
6.1.5 形式验证 87
6.2 用带时钟变量的时态逻辑来扩充Object-Z 89
6.2.1 LTLC语法 91
6.2.2 LTLC语义 92
6.2.3 扩充的Object-Z的语法 95
6.2.4 扩充的Object-Z的语义 99
6.2.5 完成的时间 102
6.2.6 实例研究 104
6.2.7 形式验证 107
6.3 小结 108
第七章 证明责任产生器的实现 110
7.1 验证系统的结构 110
7.2 验证系统的实现 111
7.2.1 Object-Z编辑器 111
7.2.2 证明责任产生器 111
7.2.3 两个实例 115
7.3 小结 119
第八章 结论与展望 120
8.1 本文主要的工作 120
8.2 将来的工作 121
参考文献 123
附录 证明责任产生器的核心源代码 135
作者在攻读博士学位期间公开发表的论文 170
作者在攻读博士学位期间所参与的项目 171
致谢 172