A Workflow Verification Method Based on Calculus.

Awareness of the need for process orientation in IT support field has been increasing these decades, which made the formalization and verification of workflow become more and more significant. Among various formal methods, calculus, a branch of process algebra, proved to be most capable in modeling mobility and interaction, therefore is considered as a good choice of workflow formalizing and verifying. In this paper, a pi-calculus-based workflow verification method is introduced, by which three kinds of structure conflicts (deadlock, lack of synchronization and cycle without exit) can be detected. Verification algorithm based on reduction and replacement rules is also provided, according to which complex workflow model with both cyclic and overlapping structures can be verified with acceptable complexity.