Humboldt-Universitat zu Berlin
The authors report on a case study on control-flow analysis of Business Process Models. They checked 735 industrial Business Process Models from financial services, telecommunications and other domains. They investigated these models for soundness (absence of deadlock and lack of synchronization) using three different approaches: the business process verification tool Woflan, the Petri net model checker LoLA, and a recently developed technique based on SESE decomposition. They evaluate the various techniques used by these approaches in terms of their ability of accelerating the check. Their results show that industrial Business Process Models can be checked in a few milliseconds, which enables tight integration of modeling with control-flow analysis.