Correctness of artefact-centric business process models

Abstract

The verification of business process models is an important step in the design phase of process-aware information systems. Currently, in the area of artefact-centric process model verification, the focus has been on the static formal analysis of process executions. However, seldom have they considered the correctness of artefact-centric business process models themselves from both structural and behavioural perspectives. In this paper, we fill this gap by introducing the concept of correctness for artefact-centric business process models from both structural and behavioural aspects. In artefact-centric modelling approach, a business process is modelled as the interaction of the involved artefact lifecycles. Therefore, the correctness of the associated artefact lifecycle models is the foundation of the correctness of an artefact-centric process model. Both structural soundness and behavioural soundness of artefact lifecycle models are proposed and the corresponding verification approaches are proposed, based on which the correctness of an artefact-centric business process model can be identified. Our work contributes to the identification of correctness issues in artefact-centric business process models in the early design or modelling phase.