Model Checking of Workflow Schemas

13 years 7 months ago
Model Checking of Workflow Schemas
Practical experience indicates that the definition of realworld 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 presents an approach 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 can then be analysed and checked for safety and liveness properties. The model generation and the analysis procedure are governed by well-defined rules that can be fully automated. Therefore, the approach is accessible by designers who are not experts in formal methods.
Christos T. Karamanolis, Dimitra Giannakopoulou, J
Added 31 Jul 2010
Updated 31 Jul 2010
Type Conference
Year 2000
Where EDOC
Authors Christos T. Karamanolis, Dimitra Giannakopoulou, Jeff Magee, Stuart M. Wheater
Comments (0)