Niels LohmannKarsten Wolf
Dirk FahlandCédric FavreJana KoehlerHagen Völzer
Barbara Jobstmann
IBM Research Zürich EPF Lausanne Universität Rostock Humboldt-Universitätzu Berlin
2
Analysis o
n Dem
and?
code generation .bpel
simulation
workflow engine
Find errors as early as possible
business processmodeler
X
business processmodel
�
error in process model
�
� unreliable simulation results
� �
� erroneous translation
find control-flow errors: check soundness
find errors as early as possible
�
� erroneous execution
3
Analysis o
n Dem
and?
sound?
Finding errors in practice
� an example from practice, not well-structured��
automated analysisneed:
on every save, load, export, on demandhow often?
how fast?press a button … < 500 ms
Which techniques allow analysis on demand?
4
Analysis o
n Dem
and?
Outline
� Soundness and how difficult is it?
� Techniques for efficient analysis
� Experimental results
5
Analysis o
n Dem
and?
A
B
C
DX
P1:
Error (1): Lack of Synchronization
AB
Lack of Synchronization:two tokens on one edge
C D D
Naïve analysis: build state space and find error state
sound = no deadlock + no lack of synchronization
State Space of P1:
C
CD
DBB
6
Analysis o
n Dem
and?
Error (2): Deadlock
A
B
C
X D
P2:
Deadlock:token cannot proceed
sound = no deadlock + no lack of synchronization
AB
C
State Space of P2:
Naïve analysis: build state space and find error state
7
Analysis o
n Dem
and?
How difficult is soundness analysis?
� 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
A XB (“free choice” constructs)
8
Analysis o
n Dem
and?
Outline
� Soundness and how difficult is it?
� Techniques for efficient analysis
� Experimental results
9
Analysis o
n Dem
and?
Partial order reduction
� 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
10
Analysis o
n Dem
and?
� decompose process into fragments (single entry and single exit)
� analyze each fragment
� error in a fragment ↔ process unsound
Refined Process Structure Tree (RPST)
A1 A2
X
B1
B2
B
AP
A: A1 A2
B
B1 B2
A
A1 A2
P
seq split/join
par
B:B1
B2
11
Analysis o
n Dem
and?
Avoid state space exploration
� heuristics on fragments, e.g.
� A: only sequence � sound
� B: one XOR-split, n0 XOR-join� unsound
� structural reduction:
� rules for reducing process model
� reduction to single node � sound
� infer behavior from model structure
� e.g. S-coverability (in Woflan) = partial check for unsoundness
A1 A2
A12
A1 A2A
X
B1
B2
B
12
Analysis o
n Dem
and?
Outline
� Soundness and how difficult is it?
� Techniques for efficient Analysis
� Experimental results
13
Analysis o
n Dem
and?
Experiment
� a sample of 735 industrial business processes
� size of processes:
� nodes: max. 118
� parallel branches: max. 66
� state space: max. >> 1,000,000
� experiment: 3 tools (different techniques)
� complete analysis on all processes
� # sound: 374 (50%)
� max. analysis time: 91 ms, avg. 10 ms
�analysis on demand
14
Analysis o
n Dem
and?
IBM WebSphere Business Modeler
Woflan
Woflan
structuralreduction
Detailed results
Petrinet
LoLA: model checker +partial order reduction
sound
unsound:error-trace
workflownet S-coverability
state spaceexploration
sound
251 processes
unsound + info
351 processes
unsound + info
sound
workflowgraph
heuristics decides 97% of all fragments
max. 50 ms
max. 91 msone exception: 1 sec
max. 62 ms
decision within 6500 statesmax. > 1,000,000
133 processes735 processes
decision within 165 states per fragment
decisionwithin 12 states
decompose(RPST)
frag-ment
IBM WebSphereheuristics
state spaceexploration
unsound:erroneousfragments
sound
15
Analysis o
n Dem
and?
Diagnostic information
� only 50% sound models
� state-space exploration� trace to error
� experiment: traces ofreasonable length
� RPST fragments� one error per fragment
� can detect multiple errors
� experiment:unsound � 2-7 error fragments
� Woflan� nodes that cause the error
A1 A2
X
B1
B2 deadlock
XB1
B2
B
XOR/AND mismatch
16
Analysis o
n Dem
and?
Conclusion
� checked soundness of 735 industrial business processes
� naïve state space exploration incomplete in practice
�apply reduction techniques (state space, structure)
� 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
17
Analysis o
n Dem
and?
Future work
� Present diagnostic information to modeler
� Check models with more involved constructs
� e.g. BPMN event handler
� Check advanced properties
� Different combinations of techniques
� RPST fragments + partial order reduction
� Try by yourself: www.service-technology.org/soundness
� process models and
� links to: LoLA / IBM WebSphere + RPST plugin / Woflan