Abstract: Concerned with Web service composition, this paper especially emphasized the formal description and verificanon of asynchronous communication behaviors and timed properties. Firstly, analyzing Web service composition from software architecture, the interactive behaviors and timed properties were described by XYZ/ADL based on temporal logic language. Secondly, timed asynchronous communication model(TACM) which accords with the specification of model checker UPPAALwas proposed. Finally, based on the transition from XYZ/RE communication command senfences to TACM, the correctness of asynchronous communication behaviors of the service composition system was verified by UPPAAI.

Key words: Web service composition,XYZ/ADI，Asynchronous communication, Timed propertics,Model checking