系统工程Petri网 建模、验证与应用指南

第一部分 Petri网——基本概念 1

第1章 引言 2

第2章 Petri网的实质特征 4

2.1 局部确定性和并发 5

2.2 图形表示和代数表示 7

2.3 并发、冲突和混惑 10

2.4 细化和组合 11

2.5 网射 16

第3章 直观模型 21

3.1 常量弧网 21

3.2 库所／变迁网 23

3.3 有色网 25

3.4 折叠 28

4.1 库所／变迁网的形式化定义 30

第4章 基本定义 30

4.2 常量弧网的形式化定义 31

4.3 有色网的形式化定义 33

第5章 性质 40

5.1 基本性质 40

5.2 分析方法介绍 44

第6章 本书总览 55

第二部分 建模 59

第7章 引言 60

第8章 实例解说建模和分析技术 62

8.1 网、优化和抽象 62

8.2 库所／变迁网和资源管理 67

8.3 有色网、抽象和展开 72

9.1 构建块 77

第9章 技术 77

9.2 结合网 79

9.3 高级网 82

9.4 分解网 85

9.5 小结 85

第10章 方法 86

10.1 面向状态建模 86

10.2 面向事件的建模 97

10.3 面向对象建模 106

第11章 实例研究 115

11.1 面向状态的方法 117

11.2 面向事件的方法 120

11.3 面向对象方法 125

第12章 小结 130

第三部分 验证 131

第13章 引言：验证所涉及的问题 132

13.1 网的分类 132

13.2 性质 135

13.3 方法分类 137

13.4 验证过程 142

13.5 概述 143

第14章 基于状态空间的方法与模型检验 144

14.1 性质、时态逻辑及公平性 144

14.2 on-the-fly方法 155

14.3 基于偏序的方法 158

14.4 符号化和参数化方法 174

14.5 实现问题 192

14.6 综合及一般性总结评注 197

第15章 结构方法 199

15.1 网系统归约 200

15.2 线性代数技术 205

15.3 虹吸和陷阱 214

15.4 网子类的分析 216

15.5 不变量和有色Petri网的归约 222

第16章 演绎与基于进程代数的方法 229

16.1 代数网的重写语义 230

16.2 断言推理 244

16.3 授权逻辑 262

16.4 线性逻辑和Petri网 268

16.5 利用进程代数验证Petri网模型 277

第17章 小结 290

第四部分 确认和执行 291

第18章 引言 292

19.1 软件生命周期和确认 293

第19章 系统工程和确认 293

19.2 确认 294

19.3 一种方法——原型建立 295

19.4 工具 298

第20章 网的运行 301

20.1 集中控制 303

20.2 将控制分发给库所 304

20.3 将控制分发给边 308

20.4 多线程和同步 309

20.5 异步 310

20.6 小结 311

第21章 代码生成 312

21.1 对于代码生成的Petri网方法 313

21.2 Petri网的划分算法 317

21.3 Petri网中代码生成的一些方面 323

21.4 高级网中的代码生成 333

21.5 小结 337

第22章 小结 339

第五部 分应用领域 341

第23章 引言 342

23.1 工作中应用Petri网 342

23.2 应用领域 342

第24章 柔性制造系统 345

24.1 领域概览 345

24.2 在FMS中使用Petri网 348

24.3 设计方法 352

24.4 小结 363

第25章 工作流系统 364

25.1 领域概述 364

25.2 动机 366

25.3 设计方法学 368

25.4 工作流分析 375

25.5 实例学习：Sagitta-2000案例 385

25.6 小结 386

第26章 电信系统 388

26.1 领域概述 388

26.2 动机 391

26.3 设计方法学 392

26.4 分析 401

26.5 小结 404

第27章 小结 405

27.1 公共建模问题 405

27.2 共享的分析结果 406

术语表 407

参考文献 422