Design, Development and Verification of a Compensable Workflow Modeling Language

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 processes and increasing productivity and quality of service. As business organizations continue to become more dependent on computerized systems, the demand for reliability has increased. Most WfMSs provide little or no verification facilities; this causes the resulting implementation of large and complex workflow models to be at risk of undesirable runtime executions. Design validation, ensuring the correctness of the design at the earliest stage possible, is a major challenge. Model checking is a promising and powerful approach to automatic verification of systems, but model checking frequently suffers from the state explosion problem and modeling with the input language of a model checker is time consuming.;To handle the state explosion problem a workflow slicing algorithm is developed and integrated into the translator. A Service Oriented Architecture (SOA) based workflow engine is designed and developed as part of the work. The effectiveness of the system has been studied by developing a workflow based on the National Principles and Norms of Practice of Canadian hospice palliative care. Finally, a sophisticated user friendly browser is discussed with which one can see records in hierarchical fashion, travel to a past record and can generate charts by selecing parameters. We show that the browser can be used as a cause and effect analysis tool, which will aid the user for root cause analysis and decision making.;To address these issues, a compensable workflow modeling language called CWML is designed and developed to provide both flexibility in the design, and also reliability in the execution of a workflow system. In this research an automated translator is developed and studied which can translate a graphical workflow model and an abstract task specification (written in Java) to the modeling language of the model checker DiVinE.