Formalization of workflows and correctness issues in the presence of concurrency

In this paper, main components of a workflow system that are relevant to th e correctness in the presence of concurrency are formalized based on set th eory and graph theory. The formalization which constitutes the theoretical basis of the correctness criterion provided can be summarized as follows: Activities of a workflow are represented through a notation based on set th eory to make it possible to formalize the conceptual grouping of activities . Control-flow is represented as a special graph based on this set definition , and it includes serial composition, parallel composition, conditional bra nching, and nesting of individual activities and conceptual activities them selves. Data-flow is represented as a directed acyclic graph in conformance with th e control-flow graph. The formalization of correctness of concurrently executing workflow instanc es is based on this framework by defining two categories of constraints on the workflow environment with which the workflow instances and their activi ties interact. These categories are: Basic constraints that specify the correct states of a workflow environment . Inter-activity constraints that define the semantic dependencies among acti vities such as an activity requiring the validity of a constraint that is s et or verified by a preceding activity. Basic constraints graph and inter-activity constraints graph which are in c onformance with the control-flow and data-flow graphs are then defined to r epresent these constraints. These graphs are used in formalizing the interv als among activities where an inter-activity constraint should be maintaine d and the intervals where a basic constraint remains invalid. A correctness criterion is defined for an interleaved execution of workflow instances us ing the constraints graphs. A concurrency control mechanism, namely Constraint Based Concurrency Contro l technique is developed based on the correctness criterion. The performanc e analysis shows the superiority of the proposed technique. Other possible approaches to the problem are also presented.