A. Happens, = 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

R. Akkiraju, D. Flaxer, H. Chang, T. Chao, L. Zhang et al., 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.

M. Baglioni, U. Ferrara, A. Romei, S. Ruggieri, and F. Turini, Use soap-based intermediaries to build chains of web service functionality, 2002.

A. Bouhoula, E. Kounalis, and M. Rusinowitch, SPIKE, an automatic theorem prover, Proceedings of LPAR 92, number 624 in LNAI, 1992.
DOI : 10.1007/BFb0013087

P. Brittenham, J. Clune, J. Durand, L. Kleijkers, K. Sankar et al., Ws-i analyzer tool functional specification

H. Foster, S. Uchitel, J. Magee, and J. Kramer, Compatibility verification for Web service choreography, Proceedings. IEEE International Conference on Web Services, 2004., p.738, 2004.
DOI : 10.1109/ICWS.2004.1314806

X. Fu, T. Bultan, and J. Su, 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

R. Irani, Web services intermediaries adding value to web services, 2001.

M. Koshina and F. Van-breugel, Verification of business processes for web services

R. Kowalski and M. J. Sergot, A logic-based calculus of events, New Generation Computing, vol.10, issue.No. 2, pp.67-95, 1986.
DOI : 10.1007/BF03037383

S. Nakajima, 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

J. Punin, M. Krishnamoorthy, and M. Zaki, Web Usage Mining ??? Languages and Algorithms, Studies in Classification, Data Analysis, and Knowledge Organization, 2001.
DOI : 10.1007/978-3-642-55721-7_28

J. Rao, P. Küngas, and M. Matskin, Logic-based web services composition: From service description to process model, ICWS, pp.446-453, 2004.

M. Rouached, W. Gaaloul, W. M. Van-der-aalst, S. Bhiri, and C. Godart, 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

M. Rouached, O. Perrin, and C. Godart, Towards formal verification of web service composition, Forth International Conference on Business Process Management (BPM06), 2006.
URL : https://hal.archives-ouvertes.fr/inria-00114012