Dependable Workflow Technology Gerhard Weikum University of the Saarland, Germany [email protected] http://www-dbs.cs.uni-sb.de/ Gerhard Weikum 1 Guiding Mottos - 20 Years Ago and Now 1983: We dont know where we are heading, but we want to be there first! 2002: Time to market is everything! Gerhard Weikum 2 Conclusion

Time to market, featurism, and $$$ Dependability and service guarantees ??? gears to build highly dependable systems Shift with predictable, guaranteed behavior !!! Dependable workflow technology: Provably correct behavior World-wide failure masking QoS with Guaranteed autonomic systems Gerhard Weikum http://www-dbs.cs.uni-sb.de/~mlite/3 What I Can Offer Overview of the area Relevant foundations Logic, formal spec, verification Fault-tolerant computing Stochastic performance modeling Interesting research problems

What Do You Want? Gerhard Weikum 4 Outline Part A: WF Specification and Verification Part B: WF System Architecture and Configuration What Is It All About? WF Specification Techniques Statecharts CTL and Model Checking Summary and WF Execution Infrastructure Failure Handling Stochastic Modeling WF System Configuration Summary and

Open Research Issues Gerhard Weikum Open Research Issues 5 Outline Part A: WF Specification and Verification Part B: WF System Architecture and Configuration What Is It All About? WF Execution Infrastructure Failure Handling Stochastic Modeling WF System Configuration Summary and WF Specification Techniques

Statecharts CTL and Model Checking Summary and Open Research Issues Gerhard Weikum Open Research Issues 6 Workflow Application Example 1: Credit Request Processing Enter Credit Request Check Credit Worthiness Make Decision Check Risk

Gerhard Weikum 7 Workflow Application Example 2: Journal Refereeing Process Choose referees Receive submitted paper Gerhard Weikum Contact referee 1 Send paper Contact referee 2 ...

Contact referee 3 ... Remind referee 1 Receive review 1 Make editorial decision Notify author 8 What is Workflow Management? Computer-supported business processes: coordination of control and data flow between distributed - automated or intellectual - activities Application examples: Credit requests, insurance claims, etc. Tax declaration, real estate purchase, etc.

Student exams, journal refereeing, etc. Electronic commerce, virtual enterprises, etc. Gerhard Weikum 9 Workflow Management System Architecture Workflow specification Ms2.lnk Gerhard Weikum Workflow server Ms1.lnk ... Applications Ms3.lnk

10 Workflow Management System Architecture Baroque Workflow specification specification Workflow server Nonscalable performance Failure-prone execution Ms2.lnk Gerhard Weikum Ms1.lnk ... Applications

Ms3.lnk 11 The Great Vision Make e-Business as simple as amoeba business ! And, as amoebas, youll have no problems recruiting other sales reps ... just keep dividing and selling, dividing and selling. Gerhard Weikum 12 Business Benefits of Workflow Technology Business process automation (to the extent possible and reasonable) shorter turnaround time, less errors, higher customer satisfaction better use of intellectual resources for exceptional cases

Transparency understanding & analyzing the enterprise Fast & easy adaptation Business Process Reengineering (BPR) Gerhard Weikum 13 Technical Benefits of Workflow Technology Application Integration (by loose coupling of activities) without having to tackle enterprise-wide data integration problems supports incremental long-term migration from stand-alone applications to electronic processes Support for Legacy Applications by wrapping them into business activities Extends Transactions to Long-lived Processes Scalability, Reliability, Availability, Manageability Gerhard Weikum 14

Workflow Management Systems (WFMS): Products and Research Prototypes BizTalk (MS) Staffware Changeengine / E-Speak (HP) jFlow / WebLogic (BEA) InConcert (Tibco) SAP Workflow

Wide and CrossFlow (EU projects) Adept (U Ulm) Wasa (U Muenster)) Opera (ETH Zurich) Mentor-lite (U Saarland) CMI (MCC) Meteor (U Georgia) ... MQSeries Workflow / WebSphere (IBM) ... + workflow technology embedded in E-Commerce products and ERP systems Gerhard Weikum 15 WfMC Reference Architecture

Workflow Management System (WFMS) Administration & Monitoring Tools Process Definition Tools Workflow Engine Workflow Enactment Service Workflow Client Applications Gerhard Weikum Other WF Enactment Services Invoked

Applications 16 Integration with Internet Technologies XML (ebXML, ...) XML (WSFL, XLANG, ...) UDDI HTTP, DHTML WSDL, SOAP, EJB, CORBA Ms3.lnk Gerhard Weikum 17 Hard Issues and Research Directions computational complexity Blues problems (NP-complete)

business (bureaucratic) complexity Rap problems (e-complete) system complexity Techno problems (DB-complete) semantic complexity Psychedelic problems (AI-complete) Gerhard Weikum 18 Outline Part A: WF Specification and Verification Part B: WF System Architecture and Configuration What Is It All About? WF Specification Techniques WF Execution Infrastructure Failure Handling Stochastic Modeling WF System Configuration

Summary and Statecharts CTL and Model Checking Summary and Open Research Issues Gerhard Weikum Open Research Issues 19 Specification in WFMS Products ... ...

...

by powerset automaton 2: states 2S =: Z Step 3: encode SC context into extended state space of FSA by an injective mapping 3: Z B1 B2 ... Bm Z such that there is a transition from z1 to z2 in the FSA iff 3-1(z2) is a possible successor configuration of 3-1(z1) in the SC Gerhard Weikum 52 Example: From SC To FSA (1) / Budget:=1000; Trials:=1; Select Conf [Found] / Cost:=0 [!Found] CheckConfFee Check Flight

Select Tutorials Compute Fee Go [Cost Budget] Check Cost Check Airfare Check Hotel Check Hotel [Cost > Budget [Fok & Eok] & Trials 3] / Cost := ConfFee + TravelExpenses No CheckTravel Expenses [Cost > Budget &

Trials < 3] / Trials++ Gerhard Weikum 53 Example: From SC To FSA (2) 1 SelectConf, !F,!Fok,!Eok, !Bok,Tok 4 3 ... CheckConfFee, CheckTravelExpenses, F,!Fok,!Eok, Bok,Tok CheckCost, F,Fok,Eok, Bok,Tok

8 5 Go, F,Fok,Eok, Bok,Tok 6 9 CheckCost, F,Fok,Eok, Bok,!Tok CheckCost, F,Fok,Eok, !Bok,!Tok No, F,Fok,Eok, !Bok,!Tok 7 2

CheckCost, F,Fok,Eok, !Bok,Tok No, !F,!Fok,!Eok, !Bok,Tok Gerhard Weikum 54 CTL: Computation Tree Logic propositional logic formulas quantifiers ranging over execution paths modal operators referring to future states all next: exists next: all globally: AX p

EX p AG p all finally exists (inevitably): globally: AF p EG p exists finally (possibly): EF p combination: EF AG p Gerhard Weikum 55 Critical Properties of the Example Workflow formalized in CTL (Computation Tree Logic) Can we ever exceed the budget ? not EF ( in(Go) and !Bok )

AG ( not in(Go) or Bok ) Do we always eventually reach a decision ? AF ( in(Go) or in(No) ) Can the trip still be approved after a proposal that would have exceeded the budget ? EF ( (in(CheckCost) and !Bok) => ( EF (in(Go)) ) ) Gerhard Weikum 56 CTL Syntax efinition: n atomic CTL formula is a propositional logic formula er elementary propositions (i.e., Boolean variables). he set of CTL formulas is defined inductively: Every atomic CTL formula is a formula.. If P and Q are formulas then EX (P), AX (P), EG (P), AG (P), EF (P), AF (P), (P), P, PQ, PQ, PQ and PQ are formulas.. Gerhard Weikum 57 CTL Semantics (1)

Definition: Consider a set P of elementary propositions. A Kripke structure M over P is a 4-tuple (S, s0, R, L) with a finite state set S, an initial state s0 S, a transition relation R S S, a function L: S 2P that assigns true propositions to each state. Gerhard Weikum 58 CTL Semantics (2) Definition: The interpretation of formula F over elementary propositions P is a mapping onto a Kripke structure M=(S, s0, R, L) over propositions P such that the truth value of subformulas p, p1, p2 of F in state s, denoted M,s |= p, is defined as follows: (i) M,s |= p with propositional formula p holds iff p L(s); (ii) M,s |= p holds iff M,s |= p does not hold; (iii) M,s |= p1 p2 iff M,s |= p1 and M,s |= p2; (iv) M,s |= p1 p2 iff M,s |= p1 or M,s |= p2; (v) M,s |= EX p iff there exists tS with (s,t)R and M,t |= p; (vi) M,s |= AX p iff for all tS with (s,t)R M,t |= p holds; (vii) M,s |= EG p if there exists t1, ..., tk S with t1=s, (ti, ti+1)R for all i and tk=tj for some j:1j

(viii) M,s |= AG p iff for all tS with (s,t)R+ M,t |= p holds; (ix) M,s |= EF p iff there exists tS with (s,t)R+ and M,t |= p; (x) M,s |= AF p iff for all tS with (s,t)R+ there exists tS with a) (t,t)R+ or b) (s,t)R+ and (t,t)R+, such that M,t |= p holds. Gerhard Weikum 59 CTL Semantics (3) Definition: A Kripke structure M = (S, s0, R, L) is a model of formula F if F is true in s0, denoted M,s0 |= F. A formula is satisfiable if it has at least one model, otherwise it is unsatisfiable. A formula is valid (or called a tautology) if every Kripke structure over the elementary propositions of F is a model of F. Gerhard Weikum 60 Model Checking For CTL formula F and transition system (Kripke structure) M check if M is a model of F by inductively marking all states of M in which subformula q of F holds with the label q.

q be a subformula of F, let p, p1, p2 direct subformulas of q, d let P, P1, P2 be the sets of states of M with labels p, p1, p2, resp. q is an elementary proposition (Boolean variable): label all states s with qL(s) with label q q is of the form p: label S P with label q ) q is of the form p1 p2: label P1 P2 with label q ) q is of the form p1 p2: label P1 P2 with label q q is of the form EX p: label all predecessors of P with label q (i.e., all sS for which there exists xP with R(s,x) ) ) q is of the form AX p: label s with q if all successors of s are labeled with p Gerhard Weikum 61 Model Checking: EF Case (vii) q has the form EF p: solve recursion EF p p EX (EF p). (fixpoint computation Q = P pred(Q) ) Q := P; Qnew := Q pred(Q); while not (Q = Qnew) do Q := Qnew; Qnew := Q pred(Q);

od; Gerhard Weikum 62 Model Checking: EG Case (viii) q has the form EG p: solve recursion EG p p EX (EG p) : Q := P; Qnew := Q ; repeat for each s in Q do if s has successors and no successor of s is in Q then Qnew := Q - {s}; fi; od; until (Q = Qnew); Gerhard Weikum 63 Model Checking: AG Case (ix) q has the form AG p: solve recursion AG p p AX (AG p)

Q := P; repeat Qnew := Q; for each s in Q do if s has successors and one successor of s is not in Q then Q := Q - {s} fi; od; until (Q = Qnew); Alternatively, because of AG p EF (p): compute state set Q labeled EF (p) and label S Q with label q. Gerhard Weikum 64 Model Checking: AF Case (x) q has the form AF p: solve recursion AF p p AX (AF p) Q := P; repeat Qnew := Q; for each s in pred(Q) do if all successors of s are in Q then Q := Q {s}; fi; od;

until (Q = Qnew); Alternatively, because of AF p EG (p): compute state set Q labeled EG (p) and label S Q with label q. Gerhard Weikum 65 Model Checking: Example 1 AG ( not in(Go) or Bok ) 1 SelectConf, !F,!Fok,!Eok, !Bok,Tok 3 ... CheckConfFee, CheckTravelExpenses, F,!Fok,!Eok, Bok,Tok 2

4 CheckCost, F,Fok,Eok, Bok,Tok 5 CheckCost, F,Fok,Eok, Bok,!Tok 6 CheckCost, F,Fok,Eok, !Bok,!Tok 7 CheckCost, F,Fok,Eok, !Bok,Tok 8 Go, F,Fok,Eok, Bok,Tok 9 No, F,Fok,Eok,

!Bok,!Tok No, !F,!Fok,!Eok, !Bok,Tok Label with Bok : with in(Go) : with in(Go) : with (Bok in(Go)) : with AG (Bok in(Go)) : Gerhard Weikum 3, 4, 5, 8 8 1, 2, 3, 4, 5, 6, 7, 9 1, 2, 3, 4, 5, 6, 7, 8, 9 1, 2, 3, 4, 5, 6, 7, 8, 9 66 Model Checking: Example 2 AF (in(Go) in(No)) 1 SelectConf, !F,!Fok,!Eok,

!Bok,Tok 3 ... CheckConfFee, CheckTravelExpenses, F,!Fok,!Eok, Bok,Tok 2 4 CheckCost, F,Fok,Eok, Bok,Tok 5 CheckCost, F,Fok,Eok, Bok,!Tok 6 CheckCost, F,Fok,Eok, !Bok,!Tok 7

CheckCost, F,Fok,Eok, !Bok,Tok 8 Go, F,Fok,Eok, Bok,Tok 9 No, F,Fok,Eok, !Bok,!Tok No, !F,!Fok,!Eok, !Bok,Tok Label with in(Go) : with in(No) : with in(Go) in(No) : with AF (in(Go) in(No)) : Gerhard Weikum

8 2, 9 2, 8, 9 2, 4, 5, 6, 8, 9 67 Model Checking: Example 3 EF ( (in(CheckCost) and !Bok) => ( EF (in(Go)) ) ) 1 SelectConf, !F,!Fok,!Eok, !Bok,Tok 3 ... CheckConfFee, CheckTravelExpenses, F,!Fok,!Eok, Bok,Tok 2 4 CheckCost,

F,Fok,Eok, Bok,Tok 5 CheckCost, F,Fok,Eok, Bok,!Tok 6 CheckCost, F,Fok,Eok, !Bok,!Tok 7 CheckCost, F,Fok,Eok, !Bok,Tok 8 Go, F,Fok,Eok, Bok,Tok 9 No, F,Fok,Eok, !Bok,!Tok

No, !F,!Fok,!Eok, !Bok,Tok Label with in(Go) : with EF (in(Go)) : with not in(CheckCost) or Bok : with (in(CheckCost) and !Bok) => ( EF (in(Go)) : with EF ( (in(CheckCost) and !Bok) => ( EF (in(Go)) ) ) : Gerhard Weikum 8 1, 3, 4, 5, 7, 8 1, 2, 3, 4, 5, 8 1, 2, 3, 4, 5, 7, 8 1, 2, 3, 4, 5, 7, 8 68 Guaranteed Behavior of Workflows Leverage computer-aided verification techniques for finite-state concurrent systems Efficiency gain with encoding of FSM as OBDD Further requirements: - User-friendly macros for CTL - More expressive logic

- Adding assertions on behavior of invoked apps - Adding real-time (clock variables) Preserving guaranteed behavior in distributed, failure-prone system environment System guarantees Gerhard Weikum 69 Outline Part A: WF Specification and Verification Part B: WF System Architecture and Configuration What Is It All About? WF Specification Techniques Statecharts CTL and Model Checking Summary and WF Execution Infrastructure Failure Handling

Stochastic Modeling WF System Configuration Summary and Open Research Issues Gerhard Weikum Open Research Issues 70 Summary and Open Research Issues Formal specification and verification methods are crucial if we want to have high confidence in the correctness of workflow models Statecharts and model checking are a good example Interesting research topics for graduate students: Formal semantics of XML-based workflow spec languages and automatic translation between languages Comprehensive, user-friendly workflow verification workbench Extended model checking or combinations with theorem proving & constraint solving for enhanced verification

Comprehensive framework for correctness-preserving run-time modifications of workflow specifications Gerhard Weikum 71