Abstract: To validate the data properties and time properties of Web service composition, we presented a model checking method based on data and time aware service model (DTSM). In this approach, first we translated Web service composition described by BPEL to formal model which contains data information and time information,and then translated this model to UPPAAL specification, at last the correctness of Web service composition was verified through a model　checking tool-UPPAAL.

Key words: Web service composition, Data property, Time property, BPEL, Model checking