Cédric Favre Jana Koehler Hagen Völzer Barbara Jobstmann Niels Lohmann Karsten Wolf Dirk Fahland IBM Research Zürich EPF Lausanne Universität Rostock Humboldt-Universität zu Berlin Find errors as early as possible simulation X business process modeler code generation .bpel Analysis on Demand? business process model workflow engine error in process model unreliable simulation results erroneous translation erroneous execution find errors as early as possible find control-flow errors: check soundness 2 Finding errors in practice Analysis on Demand? an example from practice, not well-structured sound? need: automated analysis ? on every save, load, export, on demand n e t f o w o h press a button … < 500 ms ? t s a f w o h Which techniques allow analysis on demand? 3 Outline Analysis on Demand? Soundness and how difficult is it? Techniques for efficient analysis Experimental results 4 Error (1): Lack of Synchronization P1: B A D X Lack of Synchronization: two tokens on one edge Analysis on Demand? sound = no deadlock + no lack of synchronization C State Space of P1: D A B D C C C B D B D Naïve analysis: build state space and find error state 5 Error (2): Deadlock P2: B A D X Deadlock: token cannot proceed Analysis on Demand? sound = no deadlock + no lack of synchronization C State Space of P2: A B C Naïve analysis: build state space and find error state 6 How difficult is soundness analysis? A B X (“free choice” constructs) Analysis on Demand? a sample of 735 industrial business processes all expressed with: analysis by naïve state space exploration: intractable for 4 processes only problem: state space explosion n parallel activities 2n states found 4 sound processes with >> 1,000,000 states naïve analysis is incomplete in practice 7 Outline Analysis on Demand? Soundness and how difficult is it? Techniques for efficient analysis Experimental results 8 Partial order reduction Analysis on Demand? naïve analysis: build each state: check if deadlock partial order reduction build only one path from entry to exit no deadlock on path no deadlock in the rest yields exponential reduction works also for lack of synchronization 9 Refined Process Structure Tree (RPST) P A A1 B A2 P B1 A B2 A1 A2 X seq par B Analysis on Demand? decompose process into fragments (single entry and single exit) split/join B1 B2 analyze each fragment A: A1 A2 B: B1 B2 error in a fragment ↔ process unsound 10 Avoid state space exploration A: only sequence sound B: one XOR-split, n0 XOR-join unsound A A1 B Analysis on Demand? heuristics on fragments, e.g. A2 B1 X B2 structural reduction: rules for reducing process model reduction to single node sound A1 A2 A12 infer behavior from model structure e.g. S-coverability (in Woflan) = partial check for unsoundness 11 Outline Analysis on Demand? Soundness and how difficult is it? Techniques for efficient Analysis Experimental results 12 Experiment nodes: parallel branches: state space: max. 118 max. 66 max. >> 1,000,000 Analysis on Demand? a sample of 735 industrial business processes size of processes: experiment: 3 tools (different techniques) complete analysis on all processes # sound: 374 (50%) max. analysis time: 91 ms, avg. 10 ms analysis on demand 13 Detailed results LoLA: model checker + partial order reduction max. > 1,000,000 decision within 6500 states workflow graph sound unsound: error-trace IBM WebSphere heuristics decompose frag-Business Modeler IBM WebSphere state space (RPST) ment exploration heuristics decides 97% of all fragments decision within 165 states per fragment Woflan workflow net 735 processes structural reduction sound 251 processes max. 50 ms sound Analysis on Demand? Petri net unsound: erroneous fragments max. 62 ms sound state space Woflan S-coverability exploration unsound + info 351 processes decision within 12 states unsound + info 133 processes max. 91 ms one exception: 1 sec 14 Diagnostic information Analysis on Demand? only 50% sound models state-space exploration trace to error experiment: traces of reasonable length A1 A2 B1 X B2 deadlock RPST fragments one error per fragment can detect multiple errors experiment: unsound 2-7 error fragments B B1 X B2 XOR/AND mismatch Woflan nodes that cause the error 15 Conclusion naïve state space exploration incomplete in practice apply reduction techniques (state space, structure) Analysis on Demand? checked soundness of 735 industrial business processes experiment with 3 different approaches max. < 91 ms per process allows for analysis on demand choose analysis technique depending on diagnostic info trace to error anti-patterns 16 Future work e.g. BPMN event handler Check advanced properties Different combinations of techniques Analysis on Demand? Present diagnostic information to modeler Check models with more involved constructs RPST fragments + partial order reduction Try by yourself: www.service-technology.org/soundness process models and links to: LoLA / IBM WebSphere + RPST plugin / Woflan 17