Continuing on with the CASCON technical papers session focused on service oriented systems, we saw a paper on Towards Workflow Verification by Leyla Naiza, Ahmed Mashiyat, Hao Wang and MacCaull Wendy of St. Francis Xavier University in Nova Scotia. The basis of this research is on model verification to ensure that the model matches the specification properties and doesn’t produce undesirable effects at runtime. The problem with testing any sort of real process model (i.e., one with more than the 5 steps that you see in a demo) is that it’s difficult to check the model for all possible states.
Their research looks at this by decomposing the process models to fundamental workflow patterns (e.g., synchronization, sequence), then translate these into DVE, the input language for DiVinE, a distributed and parallel model checker. They can then verify specific properties in the model specification, such as their example in clinical trials, “the end of the workflow (patient release) cannot be reached without 5 drug tests”. They switched from using Petri Nets to YAWL for process modeling in order to make the automated translation to DVE possible, and built the automated translator to test this model verification method. They also introduced a time extension to the translation, allowing verification of time-related properties of the process model.
I see the biggest challenge in mapping the businesses’ view of their rules onto specific properties to be tested; this linkage between business requirements and technical implementation has been with us since the beginning of systems, and it’s not clear that this research does any validation on those rules and properties themselves, making verification against them less meaningful. Furthermore, these properties are really business rules, and imply that the rules are encoded within the process model rather than externalized in a business rules system. Nonetheless, automating verification of process models is a step in the right direction for improving the quality complex process models.