论文部分内容阅读
业务流程是对组织内外各种管理逻辑的抽象和视图的描述。在业务流程管理(Business Process Management, BPM)领域，面向服务的架构(Service OrientedArchitecture, SOA)为跨组织建立业务流程提供了一整套的技术规范。业务流程建模作为BPM的重要组成部分，是业务流程整个生命周期的起点。业务流程模型的验证是检验流程模型正确性的技术，在流程投入运行前对流程模型进行验证有重要意义。业务流程的设计模型通常采用图形化的语言建模，而业务流程执行语言(Business Process Executable Language, BPEL)是BPM与SOA领域事实上的流程定义与执行语言标准。由于BPEL的控制流结构主要面向块状，使得图形化流程模型向BPEL的转换不易处理。工作流网是一种基于形式化理论的流程模型，已得到学术界的广泛接受。化简技术作为流程模型验证的重要方法，能够缓解状态空间爆炸问题，且易于实现自动化。然而针对自由选择工作流网这种重要的形式化流程模型，缺乏为其定制的化简方法。本文的研究内容分为两个部分：首先，采用图形化的统一建模语言(UnifiedModeling Language, UML)建立流程设计模型，以形式化的流程模型工作流网为理论支撑，以BPEL流程定义为目标模型，提出了基于模型转换的业务流程建模方法。第二，针对自由选择工作流网定义可靠完备的化简规则集，为这类模型的验证提供专属的化简技术；并在此基础上定义它们的合成规则集，为图形化流程模型的控制流结构分析提供理论依据。本文的具体研究成果包括以下几点：1.分别以UML组合结构图和类图建模业务流程在资源和数据方面的信息，然后分别定义组合结构图到BPEL流程参与者，以及类图到BPEL数据定义的映射规则。对控制流维度之外的业务流程信息进行建模，改进了UML流程设计模型生成BPEL的过程。2.提出以工作流网为中间模型，由UML活动图到BPEL控制流模型的转换方法。首先将活动图映射到自由选择工作流网，再将自由选择工作流网转换为可分离工作流网，最后由可分离工作流网生成BPEL控制流模型。与源模型到目标模型的直接映射相比，具有可靠的理论基础及等价性证明。3.提出自由选择工作流网转换为可分离工作流网的两种形式化方法。第一种方法分析图形化流程模型控制流结构中交叠模式的形成原因，形式化表述了传统的处理交叠模式的方法，并总结其适用范围，证明了转换的迹相等性。第二种方法在真并发等价性的概念下，提出非循环的自由选择工作流网的局部网展开算法，作为获得其可分离形式的转换方法。另外，还提供了判断两个安全网间真并发等价的充分条件。4.提出自由选择工作流网的一个可靠完备化简规则集，可靠性保证在化简过程中这类模型的行为正确性被保持，完备性保证任意一个正确的此类工作流网最终都能被化简为最简形式。为业务流程验证提供了形式化的更契合于流程模型的化简技术。5.定义自由选择工作流网的可靠完备化简合成规则集，并进一步限制这个合成规则集的应用，以保持可分离工作流网的可分离性。为自由选择及可分离工作流网这两类形式化流程模型的建模过程提供了与节点相比，精化维度不同且粒度更细的设计指导原则。