- Department of Electrical Engineering & Computer Science
Contents
1. R Milner Communication and Concurrency Prentice Hall International 1989 S Nakajima Verification of web services flows with model checking techniques In Proceedings of the First International Symposium on Cyber Worlds pages 378 386 Tokyo November 2002 IEEE Computer Society Press R De Nicola and M Hennessy Testing equivalences for processes Theoretical Computer Science 34 83 133 1984 S Narayanan and S A Mcllraith Simulation verification and automated composition of web services In Proceedings of the Eleventh International World Wide Web Conference pages 77 88 Honolulu May 2002 ACM G D Plotkin A structural approach to operational semantics Report DAIMI FN 19 Aarhus University Aarhus September 1981 G D Plotkin An operational semantics for CSP In D Bjorner editor Proceedings of IFIP Work ing Conference on Formal Description of Programming Concepts II pages 199 223 Garmisch Partenkirchen June 1982 North Holland 15 PW03 Sch99 G Piccinelli and S L Williams Workflow A language for composing web services In W M P van der Aalst A H M ter Hofstede and M Weske editors Proceedings of the International Conference on Busi ness Process Management volume 2678 of Lecture Notes in Computer Science pages 1 12 Eindhoven June 2003 Springer Verlag M Schroeder Verification of business processes for a correspondence handling center using CCS In A I Vermesan and F Coenen editors P2. T true t cannot be typed However if a process is well typed then its type is unique That is if P 11 01 and P I2 O2 then I Ig and O O2 Furthermore each type is finite That is if P J O then I and O are finite sets of links A process P satisfies the above mentioned restrictions if P I O for some J and O such that I O 4 Structural Operational Semantics In the previous section we introduced the syntax of the BPE calculus Next we present its semantics We model the BPE calculus by means of a structural operational semantics Plo81 In this approach a labelled transition system is defined by means of a collection of rules In our model we need to keep track of the values of the links The value of a link is either true false or undefined The latter we denote by L The status of the links is captured by an element of L true false L Initially all the links are undefined A labelled transition system consists of a collection of states a collection of labels and a collection of transitions In this case each state consists of a pair a BPE process or the nil process y which we will use to model successful termination and a link status That is a state is an element of PU x X As labels we use basic activities that is elements of A In the definition below we use the notation o z to denote the substitution defined by o Y z v if L and o otherwise Instead of o we o
3. activity send_bill waits until the order is shipped and then executes The process then waits to receive a payment from the customer If the payment is not received within a given period of time the process sends the customer a reminder and starts waiting again When the payment is received it is processed by the process_payment activity If the book is not in stock then an attempt is made to re stock by the replenish activity If the attempt is successful the stock is updated and the order is shipped If the attempt fails the reply is sent to the customer notifying them that the order cannot be completed We can use the CWB to verify properties like prop can_ship AG replenish EF lt ship_order gt tt prop always_check_stock AG receive_order AF lt check_stock gt tt The first property states that it is possible to ship the order after replenishing stock The second property states that at some point after the order is received the stock is checked As we mentioned before the CWB also supports such verification methods as equivalence checking and preorder checking Due to space limitation we do not provide any examples of these verification methods here We refer the reader to Kos03 Using the CWB we have successfully verified a number of business processes 7 Conclusion Let us first summarize our contributions We introduced a new calculus named the BPE calculus that contains the main control flow constructs of BPEL4WS We m
4. it is not clear how to capture DPE in CCS it can be done though since CCS is Turing complete Furthermore if the CWB detects for example that two processes are not bisimilar then it will not produce a counterexample in terms of the business processes but in terms of the underlying CCS processes Nakajima Nak02 describes how to use the SPIN model checker to verify web services flows The language used to specify the flows is WSFL Web Services Flow Language which is one of BPEL4WS s predecessors In order to do the verification using SPIN processes are first translated into the Promela specification language provided by SPIN The disadvantage of translating business processes into a generic language for verification is that it is not easy to relate the diagnostic information returned by the verification tool to the original process In the case of the BPE calculus the trace returned by the CWB is closely related to the trace in the original BPEL4WS process Another advantage of the CWB over the SPIN is that the former provides other verification methods in addition to model checking The approach in KGMW0O0 that uses the LTSA toolkit and the FSP process algebra suffers from the same weaknesses In the future we would like to investigate if our BPE calculus can be extended to include fault and compensation handlers and possibly even time 14 Aal97 Aal03 AH02a AHO02b CES86 CGKt 02 CS96 CS98 CS02 Fok00
5. CWB to adapt it to the BPE calculus 5 1 Syntax Description File The syntax description file contains the definition of the syntax of the BPE calculus The file is logically divided into three parts The first part presents the abstract syntax the second describes the concrete syntax and the third contains some additional syntactic constructs that are used to specify the rules defining the semantics The description of the abstract syntax consists of a sorts section a cons section and a funs section The sorts section lists all the types of entities of the language For the BPE calculus these include 10 sorts process pick activity join link value status The sorts process and pick correspond to the nonterminals P and Q in Definition 1 The sorts activity and link correspond to the sets A and L We also declare the sort value that extends the Boolean type with L This sort will be used to represent the value of a link The sort status corresponds to the set X that keeps track of the values of the links In the cons section of the first part constructors for the sorts are introduced For our calculus these include cons Nil unit gt process Activity activity gt process Join join process gt process Flow process process gt process Pick pick pick gt process A process can be constructed in a number of different ways For example the constructor Nil takes no argument and returns a process and the Pick co
6. collected According to the BPEL4WS definition CGK 02 a link must not create a control cycle That is the initiation of the source activity must not semantically require the completion of the target activity Obviously a control cycle gives rise to deadlock For example contains a control cycle However the absence of control cycles in BPEL4WS can be much more subtle For example lt sequence gt lt invoke operation first gt lt target linkName link gt lt invoke gt lt invoke operation second gt lt source linkName link gt lt invoke gt lt sequence gt contains a control cycle as well since second the source of link can only start once first the target of link has finished The initial goal of our research was to develop a tool that can automatically check if a BPEL4WS specification is free of deadlocks Rather than considering BPEL4WS in its full complexity we abstract from many details in particular from data The majority of the data that is manipulated in a BPEL4WS specification is data received from web services For this data we only know its type but not its value Considering all possible values would give rise to a huge number of different cases and hence would not allow us to consider any realistic BPEL4WS specification Furthermore we abstract from time This simplifies matters considerably As a drawback we cannot verify a BPEL4WS specification the behaviour of which relies on time in a
7. language for web services BPEL4WS This language has been designed to compose web services that interact over the Internet For an introduc tion to web services we refer the reader to for example Mau03 The lastest release of the BPEL4WS specification can be found in 2 BPEL4WS BPEL4WS is XML based that is its syntax is defined in terms of an XML grammar For example the BPEL4WS snippet lt invoke partnerLink shipping portType 1ns shippingPT operation requestShipping inputVariable shippingRequest outputVariable shippingInfo gt lt invoke gt invokes the web service operation requestShipping of the web service provided by the partner whose commu nication link is named shipping The details of the request including for example the destination are stored in the variable shippingRequest The acknowledgement will be stored in the container acknowledgement In BPEL4WS the basic activities include assignments invoking web service operations receiving re quests replying to requests waiting for a given amount of time and terminating the whole process These This research is supported by IBM basic activities are combined into structured activities using ordinary sequential control flow constructs like sequencing switch constructs and while loops Concurrency is provided by the flow construct For example in lt flow gt plane train lt flow gt the activities plane and train whose behaviour has bee
8. the default in BPEL4WS false or The latter represents that the transition condition is either true or false In this case the choice between true and false is nondeterministic We use c P to express that BPE process P has join condition c In BPEL4WS the join condition consists of incoming links combined by means of various Boolean operators Without lack of generality we restrict ourselves to those join conditions built from true links negation and conjunction In BPEL4WS the join condition and the incoming links of an activity are specified separately The join condition of an activity can only be evaluated once all incoming links of that activity are defined To simplify the BPE calculus we omit the separate specification of the incoming links Instead we rewrite the join condition c to contain all of the incoming links of process P For example if the incoming link of process P is not used in the join condition c of process c P then we change the join condition to be cA V 78 3 4 Syntax Before defining the syntax of the BPE calculus we first fix e a set A of external basic activities e the internal basic activity 7 e a set of basic activities A Ae U T and e an infinite set L of links DEFINITION 1 The set C of join conditions is defined by cn true l ac cAc where L The set P of BPE processes is defined by P alt Td Pl ces gt P P P P P P Q Q P P Q a P Q Q where a E A L E L c C and
9. Gla90 Hoa85 KGMWwO00 Kos03 Koz83 Mau03 Mils9 Nak02 NH84 NM02 Plo81 P1082 Acknowledgements References W M P van der Aalst Verification of workflow nets In P Az ma and G Balbo editors Proceedings of the 18th International Conference on Applications and Theory in Petri Nets volume 1248 of Lecture Notes in Computer Science pages 407 426 Toulouse June 1997 Springer Verlag W M P van der Aalst Challenges in business process management Verification of business processes using Petri nets Bulletin of the EATCS 80 174 199 2003 W M P van der Aalst and K M van Hee Workflow Management Models Methods and Systems The MIT Press 2002 W M P van der Aalst and A H M ter Hofstede Workflow patterns on the expressive power of Petri net based workflow languages In K Jensen editor Proceedings of the Fourth Workshop on the Prac tical Use of Coloured Petri Nets and CPN Tools volume 560 of DAIMI PB series pages 1 20 Aarhus August 2002 University of Aarhus E M Clarke E A Emerson and A P Sistla Automatic verification of finite state concurrent systems using temporal logic specifications ACM Transactions on Programing Languages and Systems 8 2 244 263 April 1986 F Curbera Y Goland J Klein F Leymann D Roller S Thatte and S Weer awarana Business process execution language for web services version 1 0 Available at http www ibm com developerworks library ws
10. UNIVERSITE 3 YORK mf UNIVERSITY oes lt P Ses Verification of Business Processes for Web Services Mariya Koshkina and Franck van Breugel Technical Report CS 2003 11 October 2003 Department of Computer Science 4700 Keele Street Toronto Ontario M3J 1P3 Canada Verification of Business Processes for Web Services Mariya Koshkina and Franck van Breugel York University Department of Computer Science 4700 Keele Street Toronto Canada M3J 1P3 mkosh cs yorku ca and franck cs yorku ca October 2003 Abstract A tool to verify properties like for example deadlock freedom of specifications in the business process execution language for web services BPEL4WS is presented The four key steps in the development of this tool are highlighted First of all a process algebra named the BPE calculus that captures the flow of control of BPEL4WS but abstracts from many details is introduced Secondly this BPE calculus is modelled by means of a structural operational semantics Thirdly the grammar defining the syntax of the BPE calculus and the rules defining the semantics of the BPE calculus are used as the input to the process algebra compiler PAC to produce a front end for the concurrency workbench CWB Finally this front end is used to adapt the CWB to the BPE calculus providing us with a tool to check properties of BPE processes 1 Introduction Recently IBM and Microsoft introduced the business process execution
11. a process terminates then it is not considered deadlocked since it is capable to making T transitions After we have expressed the syntax and semantics of the BPE calculus in the required format we can run the PAC It produces a new front end for the CWB Recompiling the CWB provides us with the version that is capable of analyzing BPE processes 12 6 Concurrency Workbench The concurrency workbench CWB CS96 is a powerful verification tool As we already discussed in the introduction it allows us to do equivalence checking preorder checking and model checking Now that we have extended the CWB to the BPE calculus we can apply these verification techniques to BPE processes For example we can use the CWB to check if a BPE process is deadlock free This can be done in a number of ways First of all we can express the property we want to check deadlock freedom in terms of a logic The logic used in the CWB is p calculus Koz83 extended with some computational tree logic CTL CES86 operators These operators are syntactic sugar and include e A for all possible execution paths e E there exists an execution path e G always for every state of an execution path e F eventually there exists a state in the execution path For more details about the syntax of the logic used in the CWB we refer the reader to the CWB user manual CS98 Recall that a state is deadlocked if it cannot make any transitions Therefore we can
12. bE true false ii ii It is evident that the resulting process algebra is considerably simpler and hence more manageable than BPEL4WS It captures all the features of the language related to the flow of control and abstracts from many details In BPEL4WS each link should have a unique source and a unique target Furthermore links cannot cross boundaries of a while activity That is activities inside of the while loop cannot be linked to any activities outside of the while loop We capture these restriction by means of the following very simple type system Only if a process satisfies these restriction it can be typed The type of a process P is a pair the set of links that are used as incoming in P and the set of links that are used as outgoing in P DEFINITION 2 acT a 0 0 END 0 0 P I O Lgo OUT FoP 0 0010 P 1 0 VON as PW med O P 0O I O WHILE IP 1 0 Py 11 01 P gt Iz O2 LAL O1N O02 SEQ P P L U I2 01 U O2 P 1 01 P I2 O2 honh 0 OWN Py Po L Ulz O U O2 S I A FLOW Py 11 01 P gt Iz Oz LOh 0 OWN Pi P2 h U Ig O1 U O2 I A PICK P L 01 Po Iz 02 LAh 90 Orn P P L U In O1 U O2 S I S SWITCH In the above definition we use links c to denote the set of links that occur in the join condition c Not every process can be typed For example the process 4 true t
13. bpe1l July 2002 R Cleaveland and S T Sims The NCSU concurrency workbench In R Alur and T Henzinger editors Proceedings of the 8th Conference on Computer Aided Verification volume 1102 of Lecture Notes in Computer Science pages 394 397 New Brunswick NJ July 1996 Springer Verlag R Cleaveland and S Sims The Concurrency Workbench of North Carolina User s Manual May 1998 R Cleaveland and S T Sims Generic tools for verifying concurrent systems Science of Computer Programming 42 1 39 47 January 2002 W J Fokkink Introduction to Process Algebra Springer Verlag 2000 R J van Glabbeek The linear time branching time spectrum In J C M Baeten and J W Klop editors Proceedings of the 1st International Conference on Concurrency Theory volume 458 of Lecture Notes in Computer Science pages 278 297 Amsterdam August 1990 Springer Verlag C A R Hoare Communicating Sequential Processes Prentice Hall International 1985 C Karamanolis D Giannakopoulou J Magee and S M Wheater Model checking of workflow schemas In Proceedings of the 4th International Enterprise Distributed Object Computing Conference pages 170 179 Makuhari Japan September 2000 IEEE Computer Society Press M Koshkina Verification of business processes for web services Master s thesis York University 2003 D Kozen Results on the propositional u calculus Theoretical Computer Science 27 333 354 1983 J Maurer editor Queue March 2003
14. calculus in terms of a labelled transition system is presented in Section 4 In Section 5 we describe how the syntax and semantics of the BPE calculus are used as input for the PAC to generate modules for the CWB In Section 6 we show how the CWB adapted to the BPE calculus can be used to check that a BPE process is free of deadlock In the concluding section of this paper we discuss related and future work 3 The BPE Calculus Rather than studying BPEL4WS in its full complexity we introduce the BPE calculus In the calculus we focus on the flow of control We abstract from data and time Furthermore we do not consider fault and compensation handlers 3 1 Basic Activities As we already mentioned in the introductory section of this paper BPEL4WS contains various basic activ ities We distinguish between external and internal basic activities The external basic activities involve interaction with the environment that is interaction with web services Invoking web service operations receiving requests from web services and reply to requests of web services are all external basic activities To simplify our calculus we abstract from the particulars of each of these activities All we want to express is that whenever one of these activities occurs some interaction with the environment takes place We do not distinguish between the different types of external basic activities We introduce a set Ae of external basic activities The syntax of
15. en is simply discarded DPE sets all of the outgoing links of the discarded process to false This is done in order to eliminate execution paths that will never be taken Also the switch construct performs a nondeterministic choice This time the environment has no influence on the choice The choice is made internally Therefore we label this transition with 7 The rules for pick and switch show similarities to the rules for external and internal choice in CSP P1082 The terminate activity represented by in the BPE calculus stops the whole process as soon as possible When this activity is encountered all branches of the execution are abandoned Additional rules for outgoing links the while loop sequencing and flows are introduced to model this behaviour Note that the activity f by itself is incapable of performing any transitions 5 Process Algebra Compiler Now that we have defined the BPE calculus both syntactically and semantically we are ready to use the process algebra compiler PAC CS02 As we already mentioned in the introduction the PAC is used to adapt the concurrency workbench CWB to support a new language It generates a front end written in Standard ML for the CWB The PAC takes as its input two files One file contains the description of the syntax of the language and the other file describes the semantics of the language Below we will describe these two files that the PAC will use to generate a front end for the
16. exit the loop or continue for another iteration is nondeterministic in our setting The above snippet is represented as P where the BPE process P represents the BPEL4WS activity get item In the BPE calculus we use P P2 and P P2 to denote the sequential and concurrent composition of the processes P and P2 These correspond to the sequence and flow constructs of BPEL4WS BPEL4WS also contains the pick construct lt pick gt lt onMessage partner km1 operation reply container klm reply gt fly klm lt onMessage gt lt onMessage partner air canada operation reply container air canada reply gt fly air canada lt onMessage gt lt onAlarm for P3DT10H gt time out lt onAlarm gt lt pick gt In a pick the onAlarm is optional In the above snippet the onAlarm sets a timer that triggers the activity time out if no message from either kml or air canada is received within three days and ten hours In the BPE calculus we represent the above snippet as akm 5 Pam Gair canada Fair canada E T Piime out where the external basic activities akm and Qair canada COrrespond to the receipt of messages from kml and air canada respectively The internal basic activity 7 represents that the timer expires recall that we abstract from time The BPE processes Pkim Pair canada and P ime out correspond to the activities fly klm fly air canada and time out respectively Next we look at an example of the
17. express that a state is deadlocked as deadlock not lt gt tt For a process to be free of deadlock all processes reachable from this process should be deadlock free This can be expressed as follows prop deadlock_free AG not deadlock Now we can use the model checker to verify if a process satisfies the property deadlock_free Alternatively we can also use the find deadlock button on the graphical user interface of the CWB If a deadlock is found a simulator is invoked This simulator depicts a sequence of transitions from the initial process to the one that may cause the deadlock Besides checking for deadlocks we can verify other interesting properties as well For example consider the book ordering process adapted from an example in Aal03 receive_order A EL TE ATESTE EEEE EET Eee FEAA tt tated Mth E E E AN RA E A AE AR ASTAN T NERE EN check stock calculate_price la x replenish ship_order fee send_bill bs true reply update receive_payment T 7 send_reminder process_payment In the diagram the solid arrows represent links and the dotted arrows represent the flow of control in a sequence The dotted frame denotes a flow and incorporates all of the activities in the flow The process starts when an order is received The order is processed by checking if the book is in stock and by calculating the price of the order concurrently If the book is in stock then the order is shipped The 13
18. ften write o The transitions are defined by the following rules DEFINITION 3 ACT a 0 gt v 0 Po V0 Sti Se ET true Po y o ue P 0 V 0 OUT GF false P 0 gt Y o False Po gt y o Bea d 00 ONP o V o u UP o V 0 fosei Gi Pa PY 7 6 P 0 gt ETOP o OUT ET b i o gt f 0 C c o true le gt P o gt P 0 3 JOIN C c a false P I O GON Ta Po gt y oligo SWITCH WHILE P 0 gt WHILE t o gt f Pio v 0 SEQ P Pp o Po 0 SEQ t Pao gt t 0 noe ae P P2 0 P2 0 FLOW o o Vi a Pi P2 7 Pi 0 FLOw tIl Poo gt t0 Pook Ra PICK TE Py o Pi o Paleon P gt r I2 O2 P P2 0 gt Pi o falseo Let us briefly discuss the above rules P gt Iz O2 P 1 0 IP o P P 4 o Pi Pi Pi Pi P o gt Pi 0 P20 gt PI Pao Pi vV Po gt Poh AeA Paro gt Pi P2 0 Pno gt Pho PV P20 gt Pi P30 t o gt t o Po 0 gt P3 0 P 4 01 Pi Po o P3 0 falso P 1 01 P P 0c a3 Po o false o ACT A process consisting of a single basic activity is capable of making just one transition After the basic activity has been performed the process can no longer make a
19. g links of the activity combined by Boolean operators Only when all the values of its incoming links are defined and its join condition evaluates to true an activity can start As a consequence if its join condition evaluates to false then the activity never starts We will use for example to depict that the join condition of activity a is 41 A Z2 In the above example activity a can only start after activities a and a have finished Let us consider the following activities and links In the above picture we use to depict the pick construct Note that the choice between the activities a1 az and a3 determines whether activity a4 is performed For example if a3 is chosen then a4 can never occur As a consequence the activity a4 could be garbage collected This can be achieved as follows If a pick construct is executed then we also assign false to all the outgoing links of those branches of the pick construct that are not chosen Ifthe join condition of an activity evaluates to false then the activity is garbage collected after assigning false to its outgoing links This garbage collection scheme is named dead path elimination DPE in CGK 02 Let us briefly return to the above example Assume that activity a3 is chosen Then as a result of DPE the value of the links 41 and l become false At this point the join condition of activity a4 can be evaluated Since its value is false by DPE activity a4 is garbage
20. ion of rules Their format is very similar to that of the rules in Definition 3 For example the rules for the flow construct look as follows flow_1 lt P1 s gt a gt lt nil s gt lt Pi P2 s gt a gt lt P2 s gt 11 lt Pi P2 s gt a gt lt Pi P2 s gt flow_3 lt Pi P2 s gt a gt lt Pi s gt flow_4 lt P1 P2 s gt a gt lt Pi P2 s gt In the above rules P1 P2 P1 and P2 are processes s and s contain the status of the links and a is a basic activity The rules for the join condition are join_i lt c gt P s gt t gt lt nil dpe s P gt In the above rules eval and dpe are user defined functions The function eval evaluates the join condition given the status of the links The function dpe updates the status of the links by assigning false to all outgoing links of the process P We have implemented status as a list Each element of the list contains a link and its status Whenever a new outgoing link is encountered it is added to the end of the list The list is scanned when we need to find the value of a link One of the properties we would like to check is deadlock freedom A state is deadlocked if it is incapable of making any transitions In order not to confuse a terminated state with a deadlocked state we have introduced the following rules nil_rule lt end s gt t gt lt end s gt This ensures that if
21. n essential way Finally we ignore fault and compensation handlers Abstracting from these details will simplify matters considerably and will make our objectives feasible it is very difficult if not almost impossible to carry out such a study for BPEL4WS as a whole In this paper we focus on a small language that includes all the concepts of BPEL4WS that we introduced above The language captures the flow of control of BPEL4WS As we already mentioned above we abstract from many details Furthermore we leave unspecified some syntactic categories like for example the basic activities That is we assume a set of basic activities but we do not specify their syntax The so obtained language we call the BPE calculus as it is similar in flavour to calculi like for example CCS Mil89 A BPEL4WS specification can be mapped to a BPE process in straightforward way If the resulting BPE process is free from deadlock then the original BPEL4WS specification is deadlock free as well provided that neither time nor fault and compensation handlers play an essential role in the BPEL4WS specification To verify that a BPE process is deadlock free we develop a model for the BPE calculus The predominant approach to model calculi like our BPE calculus is to give a structural operational semantics as advocated by Plotkin Plo81 In this paper we will follow this approach as well We model the BPE calculus by means of a labelled transition system The transiti
22. n left unspecified to simplify the example are concurrent The pick construct allows for selective communication Consider for example lt pick gt lt onMessage partner klm operation reply container klm reply gt fly kml lt onMessage gt lt onMessage partner air canada operation reply container air canada reply gt fly air canada lt onMessage gt lt pick gt On the one hand if a message from klm is received then the activity fly km1 is executed In that case the fly air canada activity will not be performed On the other hand the receipt of a message from air canada triggers the execution of the fly air canada activity and discards the fly km1 activity In the case that both messages are received almost simultaneously the choice of activity to be executed depends on the implementation of BPEL4WS Synchronization between concurrent activities is provided by means of links Each link has a source activity and a target activity Furthermore a transition condition is associated with each link The latter is a Boolean expression that is evaluated when the source activity terminates Its value is associated to the link As long as the transition condition of a link has not been evaluated the value of the link is undefined In this paper we will use for example true to depict that link has source as and target a and transition condition true Each activity has a join condition This condition consists of incomin
23. nal actions In the while loop P the process P can be repeated an arbitrary number of times After every iteration there is a nondeterministic choice to either stop or continue for another iteration This choice is internal and therefore the transition is labelled with 7 Recall that there is a restriction placed on linking in while loops If a process is well typed there are no incoming or outgoing links that cross the boundary of a while loop Since there cannot be any outgoing links from the loop DPE does not have to be triggered The loop can have a number of internal links Before entering the loop all of these links are undefined During the execution of the body of the loop the link values will change In order for each iteration to use links properly we need to reset them back to L after each iteration of the loop recall that I O for the while loop to be well typed The rules for sequencing are reminiscent to ones for sequential composition in ACP see for example Fok00 The rules for the flow construct are very similar to ones for composition in CCS The pick construct performs a nondeterministic choice The choice is external This means that the choice of the process is dictated by the environment The process that is capable of interacting with the environment is chosen If both processes are capable of such interaction then the choice is made randomly In both the switch and the pick construct the process that is not chos
24. nstructor takes two picks and produces a process Based on above specification the PAC will generate the actual Standard ML code for each constructor Constructors for some simple sorts are not defined in the cons section Instead they are listed in the funs section The constructors in this section are not generated by the PAC but have to be written by the user This is done to give the user an opportunity to program simple types efficiently or to re use existing code The user should also provide some functions for the semantic description We include such functions as join conditions evaluation and dead path elimination The funs section specifies the signatures for all the user defined functions In the second section the concrete syntax is specified In order to specify the concrete syntax first the tokens are defined nil gt NIL gt PAR gt gt ARROW ngn gt PLUS These tokens are subsequently used to capture the syntactic structure of the BPE calculus grammar process NIL NilQ activity Activity activity join ARROW process Join join process process PAR process Flow processi process2 pick PLUS pick Pick pick1 pick2 In the third and final section we introduce some additional syntax to specify the rules defining the semantics This rules syntax section has a format similar to the one described above 5 2 Semantics Description File The semantics is defined by means of a collect
25. ny transitions The nil process cannot make any transitions OUT The outgoing link in the process 7 b P becomes activated only when the source activity P completes that is when P equals y At this point the link status of link changes from undefined to either true or false If the transition condition is true or false then the link status is set to the value of the transition condition If the transition condition is then the link status is chosen nondeterministically This reflects the fact that the transition condition depends on data values from which we abstract and can evaluate to true in some cases and to false in other cases JOIN defined by C true o true Clo olt Cca C e a C c1 A c2 0 where c true false L ac false true L aud Cler o AC ca o true true false l false false false l To model the evaluation of join conditions we introduce a function C C gt E true false L In case that the join condition c of process P evaluates to true the process P will be executed In case that the join condition c is false the process P is skipped In addition to skipping P dead path elimination DPE is triggered in that case It sets all the outgoing links of process P to false In both WHILE SEQ FLOW PICK SWITCH END cases a T transition is used since the evaluation of a join condition and the execution of DPE are both inter
26. odelled our BPE calculus by means of a structural operational semantics The grammar defining the syntax of the BPE calculus and the rules defining the semantics of the BPE calculus were used as input of the PAC The PAC produced modules for the CWB so that the latter can be exploited for equivalence checking preorder checking and model checking of BPE processes Also in PW03 Piccinelli and Williams present a calculus for business processes that is similar to CCS That calculus is much simpler than our BPE calculus and does not include advanced synchronization patterns like DPE In our study we used a labelled transition system to model the BPE calculus Petri nets provide an alternative approach to model business processes For an overview we refer the reader to for example AH02a These Petri nets can also be used as a basis to develop verification tools For an example we refer the reader to Aal97 NM02 We believe that labelled transition systems are superior to Petri nets when it comes to modelling BPEL4WS since as also pointed out in AH02b advanced synchronization patterns like DPE cannot easily be captured by means of Petri nets In Sch99 Schroeder presents a translation of business processes into CCS Subsequently the CWB can be used for verification The business process language that is studied in that paper is considerably simpler than BPEL4WS It is not clear to us if this approach is also applicable to BPEL4WS In particular
27. ons of the systems are defined by a collection of rules Which rules apply to a BPE process depends on its structure An alternative approach to model business processes namely by means of Petri nets AH02a is discussed in the concluding section of this paper To verify that BPE processes are deadlock free we will exploit the Concurrency Workbench CWB CS96 Originally the CWB was designed for CCS processes The CWB supports three basic types of verification methods equivalence checking preorder checking and model checking Equivalence checking allows us to verify whether processes are behaviourally equivalent The CWB supports a number of differ ent behavioural equivalences including trace equivalence and bisimilarity see for example Gla90 for an overview of different behavioural equivalences Preorder checking is very similar to equivalence checking In this case one can check if processes are related according to some behavioural preorder like the ones induced by may and must testing see for example NH84 for more details about these testing scenarios In model checking one verifies if a process satisfies a property In the CWB the property needs to be expressed in the p calculus Koz83 Deadlock freedom can be expressed in the p calculus and hence the CWB can check if a CCS process is free of deadlock Due to its modular design the CWB can be extended to support other calculi besides CCS By adapting the CWB to the BPE calcul
28. roceedings of European Symposium on Validation and Verification of Knowledge Based Systems and Components pages 1 15 Oslo June 1999 Kluwer 16
29. switch construct lt switch gt lt case condition bpws getContainerProperty trip distance gt 500 gt plane lt case gt lt case condition bpws getContainerProperty trip distance lt 500 gt train lt case gt lt switch gt Since we abstract from data the conditions are not represented in the corresponding BPE process All we represent is that one of the cases is chosen This choice is nondeterministic The above snippet is represented as Tolare Prrain where the processes Polane and Pirain correspond to the activities plane and train Both the pick and the switch construct involve a choice For the former construct this choice depends on the environment whereas for the latter it does not The calculus CSP Hoa85 also contains both choice constructs The former is known as external choice and the latter as internal choice 3 3 Links Transition Conditions and Join Conditions As we already explained in the introduction links are used to provide synchronization between concurrent activities We use 1 b P to denote that BPE process P has link as an outgoing link That is P is the source of Z In 1 b P we use b to represent the transition condition associated to In BPEL4WS the transition condition is an arbitrary Boolean expression However since we abstract from data in the BPE calculus we only consider three transition conditions In the BPE calculus a transition condition is either true which is
30. these external basic activities is left unspecified The concept of a external basic activity in the BPE calculus is analogous to that of an action in calculi like for example CCS An internal basic activity does not interact with the environment One internal basic activity deserves some special treatment We will discuss that basic activity below The other internal basic activities are the empty activity assignments and waiting for a given amount of time Since neither data nor time is considered in our calculus the effect of these basic activities is not observable in our setting All these internal basic activities are represented by 7 in our calculus again our use of 7 is very similar to its use in calculi like for example CCS In our calculus we denote the terminate activity by Execution of this internal basic activity effects the whole process As a result the whole process stops as soon as possible 3 2 Structured Activities In the introduction we already discussed the structured activities of BPEL4WS On the basis of simplified BPEL4WS examples we will show how they are represented in the BPE calculus We first consider the while loop lt while condition bpws getContainerProperty order items gt 10 gt get item lt while gt Since we abstract from data the condition is not represented in the corresponding BPE process All we represent is that the body of the loop is executed a number of times The choice to either
31. us we obtain a tool that not only can verify if a BPE process is deadlock free our initial goal but we can also check any other property expressible in the y calculus Furthermore we can apply equivalence checking and preorder checking to BPE processes Manually implementing new modules for support of the BPE calculus in the CWB would be a time consuming task if not for the process algebra compiler PAC CS02 The PAC is a tool designed to generate front ends for verification tools in particular for the CWB Given the syntax in the form of a grammar and the semantics in the form of the rules defining the transitions of the labelled transition system of the language the PAC produces modules to support the language in the CWB These modules include for example parsers and semantic functions The modules can then be incorporated into the CWB We use the PAC in order to generate a BPE calculus front end for the CWB The development of our tool can be summarized by means of the following picture syntax of BPE calculus semantics of BPE calculus does P satisfy property The above picture only shows model checking Note however that our tool also supports equivalence checking and preorder checking The rest of this paper is organized as follows In Section 3 we describe how we abstract from various details of BPEL4WS and we introduce the syntax of the resulting BPE calculus A structural operational semantics of the BPE
Download Pdf Manuals
Related Search