图书介绍

形式化方法导论PDF|Epub|txt|kindle电子书版本网盘下载

张广泉著著
出版社：北京：清华大学出版社
ISBN：9787302411611
出版时间：2015
标注页数：256页
文件大小：33MB
文件页数：270页
主题词：形式语言

PDF下载

点此进入-本书在线PDF格式电子书下载【推荐-云解压-方便快捷】直接下载PDF格式图书。移动端-PC端通用
种子下载[BT下载速度快]温馨提示：（请使用BT下载软件FDM进行下载）软件下载地址页直链下载[便捷但速度慢] [在线试读本书] [在线获取解压码]

点击复制MD5值：e984d6a84a8d122edf15bfca62db12be

下载说明

形式化方法导论PDF格式电子书版下载

下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。

点击复制85GB完整离线版磁力链接到迅雷FDM等BT下载工具进行下载详情点击-查看共享计划

建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！

（文件页数要大于标注页数，上中下等多册电子书除外）

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

图书目录

第1章绪论1

1.1 形式化方法的发展历程1

1.2 形式化方法的基本内容3

1.2.1 系统建模3

1.2.2 形式规约4

1.2.3 形式验证5

1.3 本章小结7

习题18

第2章程序正确性证明9

2.1 前后断言法10

2.1.1 基本概念10

2.1.2 证明方法10

2.1.3 应用举例12

2.2 公理化方法14

2.2.1 基本概念14

2.2.2 证明方法14

2.2.3 应用举例16

2.3 最弱前置条件方法19

2.3.1 基本概念19

2.3.2 证明方法22

2.3.3 应用举例24

2.4 本章小结25

习题225

上篇系统建模29

第3章迁移系统29

3.1 基本概念29

3.1.1 形式定义29

3.1.2 迁移图31

3.1.3 计算32

3.2 应用举例33

3.2.1 时序电路34

3.2.2 数据依赖系统35

3.2.3 并发和交错38

3.3 本章小结42

习题343

第4章自动机44

4.1 有穷自动机44

4.1.1 有穷状态系统44

4.1.2 形式定义46

4.1.3 判定算法52

4.2 Büchi自动机53

4.2.1 ω-有穷自动机简介53

4.2.2 Büchi自动机53

4.2.3 应用举例57

4.3 本章小结59

习题459

第5章 Petri网60

5.1 库所／变迁Petri网60

5.1.1 基本概念60

5.1.2 基本性质64

5.1.3 分析方法65

5.1.4 应用举例69

5.2 谓词／变迁Petri网70

5.2.1 基本概念70

5.2.2 应用举例70

5.3 着色Petri网72

5.3.1 基本概念72

5.3.2 应用举例73

5.4 本章小结74

习题574

中篇形式规约77

第6章时序逻辑77

6.1 线性时序逻辑78

6.1.1 LTL语法78

6.1.2 LTL语义79

6.1.3 应用举例83

6.2 分支时序逻辑85

6.2.1 CTL语法85

6.2.2 CTL语义86

6.2.3 应用举例88

6.3 区间时序逻辑简介89

6.4 本章小结91

习题691

第7章并发系统属性93

7.1 基本概念93

7.2 安全性95

7.2.1 形式定义95

7.2.2 形式描述96

7.2.3 应用举例98

7.3 活性99

7.3.1 形式定义99

7.3.2 形式描述100

7.3.3 应用举例101

7.4 本章小结102

习题7103

下篇形式验证107

第8章演绎证明107

8.1 演绎证明方法107

8.1.1 PLTL逻辑系统107

8.1.2 Manna-Pnueli演绎规则方法110

8.1.3 验证图方法112

8.1.4 应用举例113

8.2 验证工具STeP118

8.2.1 STeP简介118

8.2.2 STeP使用118

8.3 STeP应用举例121

8.3.1 建模122

8.3.2 验证124

8.4 本章小结126

习题8127

第9章模型检测128

9.1 基本概念128

9.2 模型检测算法129

9.2.1 CTL模型检测算法130

9.2.2 LTL模型检测算法140

9.3 模型检测工具及应用153

9.3.1 验证工具SPIN153

9.3.2 应用举例162

9.4 本章小结166

习题9167

第10章符号模型检测168

10.1 二叉决策图169

10.1.1 基本概念169

10.1.2 约简方法171

10.1.3 Apply操作及应用174

10.2 CTL符号模型检测177

10.2.1 基本方法177

10.2.2 验证工具SMV182

10.2.3 应用举例185

10.3 LTL符号模型检测简介187

10.4 本章小结191

习题10192

第11章概率模型检测193

11.1 概率模型193

11.1.1 离散时间马尔可夫链193

11.1.2 马尔可夫决策过程195

11.1.3 连续时间马尔可夫链197

11.2 概率时序逻辑201

11.2.1 概率计算树逻辑201

11.2.2 连续随机逻辑204

11.3 概率模型检测工具及应用206

11.3.1 验证工具PRISM206

11.3.2 应用举例221

11.4 本章小结225

习题11225

第12章实时与混成系统验证227

12.1 时间自动机227

12.1.1 语法227

12.1.2 语义228

12.2 实时逻辑229

12.2.1 时间计算树逻辑230

12.2.2 度量区间时序逻辑232

12.3 实时系统模型检测234

12.3.1 基本方法234

12.3.2 验证工具UPPAAL240

12.3.3 应用举例244

12.4 混成系统验证简介246

12.4.1 混成自动机246

12.4.2 微分动态逻辑249

12.4.3 混成系统模型检测252

12.5 本章小结253

习题12254

参考文献255