Compensable WorkFlow Nets

In recent years, Workflow Management Systems (WfMSs) have been studied and developed to provide automated support for defining and controlling various activities associated with business processes. The automated support reduces costs and overall execution time for business processes, by improving the robustness of the process and increasing productivity and quality of service. As business organizations continue to become more dependant on computarized systems, the demand for reliability has increased. The language t-calculus [8] was developed to aid in the creation and verification of compensable systems. Motivated by this we define Compensable WorkFlow nets (CWF-nets) and introduce a graphical modeling language Compensable Workflow Modeling Language (CWML). We present a case study, using CWML to model a real world scenario, translate the resulting CWF-net into DVE (the input language of the DiVinE model checker) and verify properties of interest.