Research On Formal Methods Of Web Service Data And Service Composition Based On Process Algebra

With the development of the network,Web Service has become the main technology of distributed and heterogeneous application increasingly.It is a new distributed computing model and an effective method for web data and information to be integrated.At present,Web Service has become a hotspot on computer science field.People have realized the advantage of Web Service which makes more corporations and research institutes to explore it.Since formal methods can be used to model and analyze concurrent systems,it is natural to consider applying formal methods for the modeling and development of Web Service.Web data and service composition are important to the study of Web Service. This thesis focuses on the modeling and validation of web data and service composition with formal methods based on process algebra.The study illuminates that formal models are important to ensure the correctness of web data and validate the properties of service composition.Xdπis a typical model of Web data,which describes interaction between data and processes across distributed locations.In this thesis,Xdπ-based formal model of web data was established,which includes a type system.In the model,types, expressions for type deciding and type formulas were defined.The property of subject reduction has been proved as well.Business Process Execution Language(BPEL4WS) based on orchestration is a standard language in Web Services composition.It is used in the realization of business process.Higher requirement is demanded for BPEL4WS in practical applications.The modeling method and implementing algorithm are presented based on value-passing CCS in this thesis.The modeling of an example is included as well as the verification of its unlocked property.Finally,the possible future work is explored in the last chapter.