A Model Slicing Method for Workflow Verification

Workflow systems increase productivity and quality of service; however, defects in a workflow model may have severe consequences. While model checking techniques can be used to verify the correctness of a workflow model, these techniques typically suffer from the state explosion problem. We propose a model slicing algorithm with a formal proof to address this problem. The algorithm is integrated into our NOVA Workflow framework, which facilitates design, verification, execution, and error-handling. An experimental result has been presented to show that the proposed algorithm makes the verification more efficient in terms of state space and hence for memory and time usage.