| With the development of Internet technology, Web service is more and more popular by company and personal users because of its openess, reusability and platform independence. But, single web service’s function is too simple to meet the diverse and complex business needs. So, web services composition came into being. Business process execution language, WS-BPEL for short, is one of the widely used web service composition languages.WS-BPEL is based on XML language. It composes deployed web services by the means of choreography. There is a center process which controls the oveall objective. Web service composition is a process that is complex and Error proned. So, the correctness of BPEL-based web service composition becomes the main issue in academic.This paper summaries and reviews the existing formal modeling and verification methods. The features of WS-BPEL specification is analysised in detail. LOTOS is adopt as modeling language. It models and verifies the correctness of BPEL-based web service composition. The specific work is shown as follows:(1)A general formal frame written in LOTOS is built according to the characteristics of BPEL specification. A set of modeling rules from BPEL to LOTOS is given. The basic activities and structed activities of BPEL is translated into LOTOS so that the whole BPEL process can be translated into LOTOS.(2)The properties which is concerned by user such as safety properties, liveness properties and fairness properties are modeling in temporal logic language mu-calculus. Model checker Evaluator in CADP toolset is adopt to model check that whether the system satisfy the properties. Finally, the verificaition is completed.(3)A tool which can translate BPEL specification to LOTOS language automatically is designed and developed. The emphasis is the construction of LOTOS formal frame, the mapping of BPEL basic activities and structed activities. Finally sereval cased is given to explain the availability of the tool. |
PDF Full Text Request