BPM talk (pdf) given by C dric Favre

IBM Research – Zurich
Process Management Technologies
Symbolic Execution of Acyclic Business Process Models
Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Control-flow analysis of business process models
New customer
Create
customer
record
Identify
customer
Existing customer
Code generation
(e.g. BPEL)
Retrieve
Customer
record
Update
customer
records
Execution on a
workflow engine
Simulation
Check the absence of control-flow errors in business process models:
– As early as possible: during the modeling activity
We want an efficient control-flow analysis technique that provides
diagnostic information adequate for a non verification expert
2
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Our work
Symbolic execution of acyclic business process models,
which may contain IOR-joins
Quadratic time and space complexity control-flow analysis
for acyclic processes
New type of diagnostic information
Approach to dismiss false positives that are due to data
abstraction
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Agenda
Overview
Techniques
Dismissing false positives
4
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
An example
5
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Soundness: a notion of correctness
A workflow graph is sound if it is free from deadlock and lack of
synchronization
Deadlock
Deadlock
a
– A token blocked in the graph.
+
b
Lack of Synchronization
Lack of synchronization
a
– Two tokens on the same edge.
O
b
66
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
State of the art in control-flow analysis (1/2)
Trade off between efficiency and consumability:
a.Polynomial time complexity approaches that have to limited diagnostic
information (Rank theorem and reduction approaches)
b.State space exploration based approaches that return an error trace as
diagnostic information
UNSOUND
77
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
State of the art in control-flow analysis (2/2)
Trade off between efficiency and consumability:
a.Polynomial time complexity approaches that have to limited diagnostic
information (Rank theorem and reduction approaches)
b.State space exploration based approaches that return an error trace as
diagnostic information
88
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
State of the art in control-flow analysis (2/2)
Trade off between efficiency and consumability:
a.Polynomial time complexity approaches that have to limited diagnostic
information (Rank theorem and reduction approaches)
b.State space exploration based approaches that return an error trace as
diagnostic information
Lack of synchronization
on this edge
99
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution (1/3)
New customer
Is gold customer
Show error graphically as reduced error trace
Edges get labeled with conditions under which they carry a token
– Allow us to reason about the condition under which the error can occur
User can decide whether an error can occur in practice: dismiss or repair
Quadratic time and space complexity
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution (2/3)
Is gold customer OR
New customer
Is not gold customer
Show error graphically as reduced error trace
Edges get labeled with conditions under which they carry a token
– Allow us to reason about the condition under which the error can occur
User can decide whether an error can occur in practice: dismiss or repair
Quadratic time and space complexity
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution (3/3)
Show error graphically as reduced error trace
Edges get labeled with conditions under which they carry a token
– Allow us to reason about the condition under which the error can occur
User can decide whether an error can occur in practice: dismiss or repair
Quadratic time and space complexity
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Agenda
Overview
Techniques
– Lack of synchronization detection and trace display
– Conditions and deadlock detection
Dismissing false positives
13
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Handles
Two disjoint paths between an IOR-split or an AND-split
and an XOR-join [EsparzaSilva, Aalst]
O
+
In a deadlock free acyclic business process model, there is
a lack of synchronization if and only if there is a handle.
14
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Handles: An adequate diagnostic information.
Executing a handle results in a lack of synchronization
In acyclic processes, handles can be detected in quadratic
time using a modified graph theoretical approach.
15
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Agenda
Overview
Techniques
– Lack of synchronization detection and trace display
– Conditions and deadlock detection
Dismissing false positives
16
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Characterization of an execution
In an acyclic process, an execution is characterized by the
conditions that are evaluated to true
Evaluated to true: New customer, Is not gold customer,
and Not eligible
17
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Characterization of an execution
In an acyclic process, an execution is characterized by the
conditions that are evaluated to true
New customer
Create
customer
record
Identify
customer
Is gold customer
Existing customer Retrieve
Customer
record
Update
customer
records
Check
customer
status
Deduct 2%
of bill
Add free
gift
Add
taxes
Is not gold customer
Is not gold customer
Check eligibility to
become gold
customer
Eligible
Not eligible
Evaluated to true: New customer, Is not gold customer,
and Not eligible
18
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic Execution
Characterizes the set of executions that lead an edge to
carry a token in terms of conditions
Is gold customer OR
New customer
19
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Example
Propagation rules:
+
O
O
+
O
+
+
+
O
20
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic Execution – Detecting deadlocks
A symbol maps to a set of executions
Multiples symbols are equivalent, i.e., map to the same set of executions
To check the absence of deadlock at an AND-join, we check that the
incoming edges carry equivalent symbols
To check edge equivalence, check symbol equivalence by computing the
maximal symbol of each symbol
– Largest symbol such that it is equivalent to the original symbol
– Normal form of the equivalent symbols
21
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
22
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
23
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
24
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
25
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
26
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
27
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
28
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
29
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
30
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
31
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
32
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
+
+
+
O
33
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Symbolic execution - Continued
Propagation rules:
+
O
O
+
O
O
34
+
+
+
Computation of the maximal
symbol in linear time
Symbolic execution in
quadratic time
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Agenda
Overview
Techniques
Dismissing false positives
35
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
False positives
New customer
Is gold customer
O
36
Some information not contained in the
business process model
Conditions are abstracted during the
analysis
Lead to detect errors that cannot
happen in an ‘actual’ execution
+
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Dismissing false positives via user interaction
+
O
37
+
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Not every error should be dismissed
Every edge should be marked during a sound execution
(relaxed soundness [DehnertRittgen])
Heuristics for errors that should not be dismissed
– Deadlock without handle when replacing AND-join by an XOR-join
– Lack of synchronization where a condition occurs in multiple
maximal symbols
+
38
O
+
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
O
© 2010 IBM Corporation
IBM Research – Zurich
Process Management Technologies
Conclusion
Symbolic execution
– of acyclic business process models that may contain IOR-joins
which allows to characterize the execution that mark an edge
– Leads to a control-flow analysis with a new type of diagnostic
information in term of conditions and which has quadratic time
complexity
– Approach to dismiss false positives that are due to data abstraction
– Provide control-flow relationships that are useful beyond controlflow analysis (e.g. data-flow analysis)
Future work:
– Cyclic business process models
– Composition of business process models
– Data-flow analysis
39
Symbolic Execution of Acyclic Workflow Graphs - Cédric Favre and Hagen Völzer
© 2010 IBM Corporation
Similar pages