Soundness verification for conceptual workflow nets with data: Early detection of errors with the most precision possible

A conceptual workflow model specifies the control flow of a workflow together with abstract data information. This model is later on refined by adding specific data information, resulting in an executable workflow which is then run on an information system. It is desirable that correctness properties of the conceptual workflow are transferable to its refinements. In this paper, we present classical workflow nets extended with data operations as a conceptual workflow model. For these nets, we develop a novel technique to verify soundness. An executable workflow is sound if from every reachable state it is always possible to terminate properly. Our technique allows us to analyze a conceptual workflow and to conclude whether there exists at least one sound refinement of it, and whether any refinement of a conceptual workflow model is sound. The positive answer to the first question in combination with the negative answer to the second question means that sound and unsound refinements for the conceptual workflow in question are possible.

► We introduce a generalized model for conceptual workflows with data.
► We define a method for checking soundness of conceptual workflows with data.
► We diagnose whether the workflow is sound for any, for some, or for no refinement.
► We also cover the coverability analysis, achieving the most precision possible.
► The analysis is based on the use of may-/must-semantics.