A Formal Model For Declarative Workflows: Dynamic Condition Response Graphs

Current business process technology is pretty good in supporting well-structured business processes and aim at achieving a fixed goal by carrying out an exact set of operations. In contrast, those exact operations needed to fulfill a business pro- cess/workflow may not be always possible to foresee in highly complex and dynamic environments like healthcare and case management sectors, where the processes ex- hibit a lot of uncertainty and unexpected behavior and thereby require high degree of flexibility. Several research groups have suggested declarative models as a good approach to handle such ad-hoc nature by describing control flow implicitly and there by offering greater flexibility to the end uses.
The first contribution of this PhD thesis is to formalize the core primitives of a declarative workflow management system employed by our industrial partner Resultmaker and further develop it as a general formal model for specification and execution of declarative, event-based business processes, as a generalization of a concurrency model, the classic event structures. The model allows for an intuitive operational semantics and mapping of execution state by a notion of markings of the graphs and we have proved that it is sufficiently expressive to model ω-regular languages for infinite runs. The model has been extended with nested sub-graphs to express hierarchy, multi-instance sub processes to model replicated behavior and support for data.
The second contribution of the thesis is to provide a formal technique for safe distribution of collaborative, cross-organizational workflows declaratively modeled in DCR graphs based on a notion of projections. The generality of the distribution technique allows for fine tuned projections based on few selected events/labels, at the same time keeping the declarative nature of the projected graphs (which are also DCR graphs). We have also provided semantics for distributed executions based on synchronous communication among network of projected graphs and proved that global and distributed executions are equivalent.
Further, to support modeling of processes using DCR Graphs and to make the formal model available to a wider audience, we have developed prototype tools for specification and a workflow engine for the execution of DCR Graphs. We have also developed tools interfacing SPIN model checker to formally verify safety and liveness properties on the DCR Graphs. Case studies from healthcare and case management domains have been modeled in DCR Graphs to show that our formal model is suitable for modeling the workflows from those dynamic sectors.
This PhD project is funded by the Danish Strategic Research Council through the Trustworthy Pervasive Healthcare Services project (www.trustcare.eu).