第一章 前言 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