Web service composition is the hotspot in the field of Web services.Many methods are proposed to describe and verify its correctness.This paper researches specification and verification of Web services composition from software architecture.Refinement checking and model checking are two important formal verification methods.This paper explores the problem of Web service composition based on both software architecture description language XYZ/ADL and formal verification

then proposes a specification and verification method of Web service composition. XYZ/ADL is the extension of the temporal logic language XYZ/E.Considering most Web service with real time characteristics

we can use XYZ/RE which is the real time extension of XYZ/E to express time constraints of the system.For systems with time constraints

we transform the system description to corresponding timed automata according to the mapping rules

then use refinement checking and model checking to verify the correctness of web service composition.Experiments demonstrate feasibility and validity of above idea.