Abstract: BPEL is often used to describe the composition of Web Services, but it is lack of sound formal semantic. Web services were prone errors. Based on Timed Color Petri Net, transitions from Web Services which was described using I3PEL to Timed Color Petri Net models were proposed, while I3PEL activities execute ways and environments were considered. The models we get arc more exacter and can be used to verify and test Web Service. An instance of this transition were gmen.

Key words: Web Service,BPEL, Model, Process verify