● 摘要
传统的工作流管理系统在流程定义的时候隐含假设了所有的活动和它们之间的协作关系能被事先准确、完善地定义好，一旦模型建立好，工作流管理系统就会按照模型规定的业务流程执行。但是随着企业经营环境与业务需求的不断变化，不得不对业务流程不断地调整。显然，传统的工作流管理系统是适应不了新的情况。约束工作流模型使用声明性的语言来描述模型，建立起的模型本身就有很大的柔性，能够有效地避免变更。在不得不进行变更的情况下，约束工作流模型能够方便简单地进行模型变更和实例迁移，脱离了过程性模型在变更时极其复杂的方法。本文在约束工作流理论和方法的基础上，使用线性时序来描述模型中的约束。利用线性时序逻辑的特性，解决了约束工作流模型的验证问题，保证了建立好的模型中不包含冲突和死活动。在上述方法的基础上，本文改进了线性时序逻辑的语义和自动机的定义，使得产生的自动机能够验证有穷序列，解决了约束工作流引擎执行和模型动态变更后实例迁移的问题。线性时序逻辑很难理解与使用，论文定义了存在型模板、关系型模板、否定型模板和选择型模板，解决了用户使用线性时序逻辑建模困难的问题。最后，设计并实现了一个基于线性时序逻辑的约束工作流管理系统的原型。用户可以通过图形化的界面，使用模板方便地进行建模，系统会自动对模型进行验证，找出模型中存在的冲突和死活动。在流程执行过程中，用户可以实时监控每个约束的状态。当流程模型发生变化时，能够验证是否能把运行实例迁移到新模型上并实施有效迁移。