面向对象软件的形式验证技术PDF电子书下载
- 电子书积分:9 积分如何计算积分?
- 作 者:文志诚著
- 出 版 社:上海:上海大学出版社
- 出版年份:2011
- ISBN:9787811186482
- 页数:172 页
第一章 前言 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
- 《钒产业技术及应用》高峰,彭清静,华骏主编 2019
- 《现代水泥技术发展与应用论文集》天津水泥工业设计研究院有限公司编 2019
- 《异质性条件下技术创新最优市场结构研究 以中国高技术产业为例》千慧雄 2019
- 《Prometheus技术秘笈》百里燊 2019
- 《中央财政支持提升专业服务产业发展能力项目水利工程专业课程建设成果 设施农业工程技术》赵英编 2018
- 《药剂学实验操作技术》刘芳,高森主编 2019
- 《林下养蜂技术》罗文华,黄勇,刘佳霖主编 2017
- 《脱硝运行技术1000问》朱国宇编 2019
- 《催化剂制备过程技术》韩勇责任编辑;(中国)张继光 2019
- 《信息系统安全技术管理策略 信息安全经济学视角》赵柳榕著 2020
- 《中风偏瘫 脑萎缩 痴呆 最新治疗原则与方法》孙作东著 2004
- 《水面舰艇编队作战运筹分析》谭安胜著 2009
- 《王蒙文集 新版 35 评点《红楼梦》 上》王蒙著 2020
- 《TED说话的力量 世界优秀演讲者的口才秘诀》(坦桑)阿卡什·P.卡里亚著 2019
- 《燕堂夜话》蒋忠和著 2019
- 《经久》静水边著 2019
- 《魔法销售台词》(美)埃尔默·惠勒著 2019
- 《微表情密码》(波)卡西亚·韦佐夫斯基,(波)帕特里克·韦佐夫斯基著 2019
- 《看书琐记与作文秘诀》鲁迅著 2019
- 《酒国》莫言著 2019