Supporting business process variability through declarative process families
提出声明式过程族概念，用于支持业务流程变异性，并给出形式化验证流程模型是否属于指定过程族的方法，帮助组织在偏离规定流程时自动验证是否允许。
Organizations use business process management systems to automate processes that they use to perform tasks or interact with customers. However, several variants of the same business process may exist due to, e.g., mergers, customer-tailored services, diverse market segments, or distinct legislation across borders. As a result, reliable support for process variability has been identified as a necessity. In this article, we introduce the concept of declarative process families to support process variability and present a procedure to formally verify whether a business process model is part of a specified process family. The procedure allows to identify potential parts in the process that violate the process family. By introducing the concept of process families, we allow organizations to deviate from their prescribed processes using normal process model notation and automatically verify if such a deviation is allowed. To demonstrate the applicability of the approach, a simple example process is used that describes several variants of a car rental process which is required to adhere to several process families. Moreover, to support the proposed procedure, we present a tool that allows business processes, specified as Petri nets, to be verified against their declarative process families using the NuSMV2 model checker. • We formally introduce the concept of declarative process family. • We formally define the distinction between weak and strong process variants. • We discuss a procedure to verify membership of a process family. • We propose a framework integrating verification relations between process models, sets of process models and their declarative specification. • We present a tool to support the presented variability and verification features.