Using TLA for modeling and analysis of Web services composition

With the evolution of service-oriented architecture, providing support for compositing distributed and autonomous Web services into business applications has become a key area in software engineering research. Flexibility of business applications will be obtained through utilizing Web services composition technologies. However, at this stage, the research on these emerging technologies dose not solve the necessary problems to build Web service compositions, especially in Web service composition modeling, composition verification, executable semantics and supporting systems. In this paper, a temporal logic named TLA (Temporal Logic of Actions ) is introduced to solve the problem of composition verification. Particularly, algorithms for the automatic translation from BPEL4WS (Business Process Execution Language for Web Services )to TLA are discussed. The aim is to use model checking to automatically verify Web service behaviors for TLA specifications which is translated from the BPEL specifications.