图书介绍
面向对象软件的形式验证技术PDF|Epub|txt|kindle电子书版本网盘下载
- 文志诚著 著
- 出版社： 上海：上海大学出版社
- 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-Z12
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/EVES45
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.Join58
4.4.2 对于O.Leave60
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-Z89
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