Verification of Time-Constrained Workflows in a Distributed Memory Environment

Correctness of workflow models is critical for the proper execution of business processes. While model checking can ensure the reliability of workflow models, the effort involved in modeling and the memory required verifying complex workflows pose a major problem. Incorporation of time constraints in a workflow model exacerbates the mentioned problems. In this thesis, we addressed these problems using two different approaches. First, we developed a tool YAWL2DVE-t (an extended version of YAWL2DVE) which can automatically translate a time-constrained workflow (with delays and durations on the tasks), built in YAWL, into the input language of the distributed model checker DIVINE, which can then verify LTL properties with time constraints of the workflow model. Second, we implemented the Property Driven Nested DFS [4] algorithm to verify LTL properties with timing information of a workflow model in a distributed memory environment. We proposed a slightly modified notion of Time Petri Nets, called Explicit Time Petri Nets (ETPN), motivated by the time constraints for workflows and Lamport's explicit time description method. We discussed a conceptual model for designing time-constrained workflow and its relationship to ETPN. In our case study, we used a time Petri Nets-based tool, Romeo, for designing the workflow; the semantics of the model is based on ETPN. This distributed verification method can take a time-constrained workflow (conceptualized as an ETPN model), generate the state space over the workstations of a computer cluster and verify LTL properties with time constraints where time is simulated as part of the states. We conducted the case study on both approaches and found that the first one gives better performance than the second. However, there is a lot of scope for optimizing and enhancing the verification method used in second approach.