A tableau-based workflow verification framework for Computation Tree Logic (CTL).

摘要

Workflow management systems (WfMS) provide convenient ways to visualize, analyse and automate work processes. Safety critical systems must ensure an error free workflow execution to ensure the safety of the clients. While formal verification techniques can be used in the development stages to help ensure behavioral properties of such systems, such techniques are generally lacking in workflow tools. We present a framework which allows us to model workflows using a Petri net based modelling tool and translate the model to a tableau style model checker. The framework uses the recently introduced one-pass algorithm, shown to deliver enhanced performance over traditional two-pass strategies in practical applications. A failed tableau will generate a counter model which can aid in debugging. We present a case study involving a health services delivery program, and verify properties written in Computation Tree Logic (CTL).