基于Petri网与时态逻辑的工作流模型及模型验证

摘要

工作流管理系统完成工作流的定义和管理，并按照在计算机中预先定义好的工作流逻辑推进工作流实例的执行。工作流过程建模是给业务过程计算机化的表示。模型描述能力的强弱决定了系统所支持应用的范围以及系统的灵活度。Petri网适合于表达系统的行为结构，时态逻辑则擅长于描述系统的特性和约束。由于本文的目标是建立一种既可以描述工作流可操作性的行为结构又同时能方便表示出工作流系统的特性或约束需求的模型，因此采用了双语言建模方式，提出了Petri网与时态逻辑结合的工作流模型，即时态逻辑约束的工作流模型。本文提出的工作流模型增强了模型的描述能力，并对减少模型的结点冗余以及增强系统的灵活性做出了贡献。 为了避免在实际运行的过程中才发现没有可满足的运行路径，减少不必要的损失，对工作流的模型验证必不可少。文中采用了模型检测工具Spin对工作流的性质进行验证，实现了工作流模型到Spin输入语言Promela的转换，给用户提供了一个易于使用的工作流模型验证环境。

目录

文摘

英文文摘

第1章 引言

第2章 相关基础理论与技术简介

第3章 基于Petri网与时态逻辑的工作流建模

第4章 基于Petri网与时态逻辑的工作流模型性质验证

第5章 建模及模型验证实例

第6章 总结和进一步要做的工作

参考文献

附录

研究生阶段工作

致谢

论文原创性声明