CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand?...

17
Niels Lohmann Karsten Wolf Dirk Fahland Cédric Favre Jana Koehler Hagen Völzer Barbara Jobstmann IBM Research Zürich EPF Lausanne Universität Rostock Humboldt-Universität zu Berlin

Transcript of CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand?...

Page 1: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 2: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 3: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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?

Page 4: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

4

Analysis o

n Dem

and?

Outline

� Soundness and how difficult is it?

� Techniques for efficient analysis

� Experimental results

Page 5: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 6: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 7: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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)

Page 8: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

8

Analysis o

n Dem

and?

Outline

� Soundness and how difficult is it?

� Techniques for efficient analysis

� Experimental results

Page 9: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 10: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 11: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 12: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

12

Analysis o

n Dem

and?

Outline

� Soundness and how difficult is it?

� Techniques for efficient Analysis

� Experimental results

Page 13: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 14: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 15: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 16: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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

Page 17: CédricFavre Dirk Fahland Barbara Jobstmann Niels Lohmann ...€¦ · 13 Analysis on Demand? Experiment a sample of 735 industrial business processes size of processes: nodes: max.

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