工作流模型性能分析与形式化验证：一种基于扩展Petri网的方法
| 摘要 | 第1-11页 |
| ABSTRACT | 第11-12页 |
| 第一章 引言 | 第12-21页 |
| ·课题背景 | 第12-13页 |
| ·工作流性能分析与验证方法概述 | 第13-14页 |
| ·研究现状 | 第14-17页 |
| ·工作流形式化验证的研究现状 | 第14-15页 |
| ·工作流性能分析的研究现状 | 第15-17页 |
| ·问题提出与研究内容 | 第17-19页 |
| ·本文贡献 | 第19页 |
| ·大纲 | 第19-21页 |
| 第二章 背景知识 | 第21-32页 |
| ·工作流概述 | 第21-25页 |
| ·工作流及工作流管理系统 | 第21-23页 |
| ·工作流模型简介 | 第23-25页 |
| ·工作流模型形式化验证背景知识 | 第25-31页 |
| ·时态逻辑与模型检验 | 第25-30页 |
| ·可达性分析简介 | 第30-31页 |
| ·小结 | 第31-32页 |
| 第三章 支持工作流性能分析与验证的EHCPN模型 | 第32-44页 |
| ·Petri网概述 | 第32-34页 |
| ·EHCPN模型的定义 | 第34-36页 |
| ·工作流模型的语法和语义 | 第36-37页 |
| ·工作流模型到EHCPN模型的转换 | 第37-43页 |
| ·小结 | 第43-44页 |
| 第四章 基于EHCPN的工作流性能分析与验证 | 第44-60页 |
| ·使用EHCPN对工作流进行性能分析和验证的原因 | 第44页 |
| ·WF-P/TMSE仿真验证集成环境 | 第44-47页 |
| ·建模环境 | 第47-51页 |
| ·仿真环境 | 第51-53页 |
| ·模型检验器 | 第53-59页 |
| ·无穷状态空间到有穷状态空间的转换 | 第54-55页 |
| ·状态组构造算法 | 第55-57页 |
| ·模型检验器 | 第57-59页 |
| ·小结 | 第59-60页 |
| 第五章 案例分析 | 第60-71页 |
| ·仿真分析 | 第60-64页 |
| ·基本需求及有关假设 | 第60页 |
| ·系统模型 | 第60-63页 |
| ·实验及结果分析 | 第63-64页 |
| ·验证分析 | 第64-66页 |
| ·相关案例分析 | 第66-70页 |
| ·小结 | 第70-71页 |
| 结束语 | 第71-73页 |
| 全文工作总结 | 第71-72页 |
| 工作展望 | 第72-73页 |
| 致谢 | 第73-74页 |
| 参考文献 | 第74-77页 |
| 作者在学期间取得的学术成果 | 第77页 |
