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