University of Portsmouth
Business Process Management (BPM) aims at designing, enacting, managing, analyzing, and adapting business processes. This paper focuses on a special kind of analysis, called verification. Verification proves correctness of business processes regarding structural constrains like deadlocks or livelocks that require a formal semantics of the routing constructs contained in business processes. The correctness criterion investigated is called Lazy Soundness. This paper introduces a prototypic tool chain to investigate the feasibility of deciding lazy soundness for Business Process Diagrams (BPD).