点此搜书

当前位置:面向对象软件的形式验证技术pdf电子书下载 > 文化科学教育体育
面向对象软件的形式验证技术
  • 作 者:文志诚著
  • 出 版 社:上海:上海大学出版社
  • 出版年份:2011
  • ISBN:9787811186482
  • 标注页数:172 页
  • PDF页数:187 页
  • 请阅读订购服务说明与试读!

文档类型

价格(积分)

购买连接

试读

PDF格式

8

立即购买

点击试读

订购服务说明

1、本站所有的书默认都是PDF格式,该格式图书只能阅读和打印,不能再次编辑。

2、除分上下册或者多册的情况下,一般PDF页数一定要大于标注页数才建议下单购买。【本资源187 ≥172页】

图书下载及付费说明

1、所有的电子图书为PDF格式,支持电脑、手机、平板等各类电子设备阅读;可以任意拷贝文件到不同的阅读设备里进行阅读。

2、电子图书在提交订单后一般半小时内处理完成,最晚48小时内处理完成。(非工作日购买会延迟)

3、所有的电子图书都是原书直接扫描方式制作而成。

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

购买PDF格式(8分)
返回顶部