Web services are becoming more and more complex, involving numerous interacting business objects within considerable processes. In order to fully explore Web service business opportunities while ensuring a correct and reliable modelling and execution, analyzing and tracking Web services interactions will enable them to be well understood and controlled. Then, given the resulting event log we want to verify certain specified properties, to provide knowledge about the context of and the reasons for discrepancies between services'behaviours and related instances. This paper advocates a novel technique to log composite Web services and a formal approach, based on an algeabric specification of the discrete event calculus language DEC, to check behavioural properties of composite Web services regarding their execution log. An automated induction-based theorem prover SPIKE is used as verification back-end.