Modelling and analysis of workflow processes

Practical experience indicates that the definition of real-world workflow applications is a complex and error-prone process. Existing workflow management systems provide the means, in the best case, for very primitive syntactic verification, which is not enough to guarantee the overall correctness and robustness of workflow applications. The paper introduces a method for formal verification of workflow schemas (definitions). Workflow behaviour is modelled by means of an automata-based method, which facilitates exhaustive compositional reachability analysis. The workflow behaviour is checked against both safety and liveness properties, which can be either generic (applicable to all workflow schemas) or domain specific (applicable to a given schema). The analysis is performed by automated tools, which are accessible to designers who are not experts in formal methods