A pattern-based approach for the verification of business process descriptions

ContextEmpirical studies indicate that companies mostly adopt business process management to support organizational concerns. Consequently, descriptions of business processes usually rely on natural languages or tables. Nevertheless, many companies also intend to support process execution using software (e.g. ERP systems, databases, office applications). This involves significant implementation effort, and therefore the underlying business process description should be correct.ObjectiveThis paper presents an approach for verifying business process descriptions that can be presented in any style, e.g. as text, tables or graphical process model created with some or other process modelling language.MethodBecause of its generality and the availability of tools, model checking is used here to verify business process descriptions. In particular, the SPIN model checker was chosen because it is well-established and continuously improved. The proposed composition-based approach permits the semi-automatic implementation of any kind of business process description in the SPIN tool and the verification of numerous correctness properties, which refer to workflow control flow patterns, safety and liveness.ResultsBecause of systemizing, the proposed approach represents all 43 workflow control-flow patterns by 20 basic ones, six fragments and their relationships. For the basic patterns and fragments, PROMELA inline-constructs are provided, and the set of applicable correctness properties is suggested. The correctness properties are specified as templates in linear temporal logic. Implementing a business process description consists of assembling the inline-constructs and associating business semantics with the symbols in the logical formulae of the correctness properties. For verification, the SPIN algorithms are used.ConclusionBy using the approach presented, business process descriptions can be checked for correctness even if the original business process description is vague. The control structures allowed in the business process descriptions are not restricted, and the verifiable correctness properties go beyond soundness.