= true ? Initiates(event, f, t1) = true ? HoldsAt(f, t1, 0) = true (A2) HoldsAt(f, t1, t) = true?Clipped(f, t1+t, s(0)) = f alse ? HoldsAt(f, t1, s(t)) = true (A3) event = N oact ? Happens(p(event, t1)) = true ? T erminates(event, f, t1) = true ? Clipped(f, t1, s(0)) = true (A4) event = N oact?Happens(p(event, t1+t+s(0))) = true?T erminates(event, f, t1+ t + s(0)) = true ? Clipped(f, t1, s(s(t))) = true, A5) Happens(p(N oact))) = true =? Clipped(f, t1, s(s(t))) = Clipped(f, t1, t + s, p.1 ,
Only the first three steps are to be defined for every composite Web serivces. Once building the algebraic specification, we can check all behevioural properties by means the powerful deductive techniques (rewriting and induction) provided by SPIKE . References 1 A framework for enabling dynamic e-business via web service, Proceedings of the OOPSLA, 2001. ,
Use soap-based intermediaries to build chains of web service functionality, 2002. ,
SPIKE, an automatic theorem prover, Proceedings of LPAR 92, number 624 in LNAI, 1992. ,
DOI : 10.1007/BFb0013087
Ws-i analyzer tool functional specification ,
Compatibility verification for Web service choreography, Proceedings. IEEE International Conference on Web Services, 2004., p.738, 2004. ,
DOI : 10.1109/ICWS.2004.1314806
Analysis of interacting BPEL web services, Proceedings of the 13th conference on World Wide Web , WWW '04, pp.621-630, 2004. ,
DOI : 10.1145/988672.988756
Web services intermediaries adding value to web services, 2001. ,
Verification of business processes for web services ,
A logic-based calculus of events, New Generation Computing, vol.10, issue.No. 2, pp.67-95, 1986. ,
DOI : 10.1007/BF03037383
Verification of Web service flows with model-checking techniques, First International Symposium on Cyber Worlds, 2002. Proceedings., pp.378-385, 2002. ,
DOI : 10.1109/CW.2002.1180904
Web Usage Mining ??? Languages and Algorithms, Studies in Classification, Data Analysis, and Knowledge Organization, 2001. ,
DOI : 10.1007/978-3-642-55721-7_28
Logic-based web services composition: From service description to process model, ICWS, pp.446-453, 2004. ,
Web service mining and verification of properties: An approach based on event calculus, Proceedings 14th International Conference on Cooperative Information Systems, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00114023
Towards formal verification of web service composition, Forth International Conference on Business Process Management (BPM06), 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00114012