| Service-oriented architecture(SOA)is an emerging software architecture and a way to build distributed systems that provide functionality as services and emphasize loose coupling between services.Web service is the basic unit of SOA architecture and a new type of Web application.With the rapid development of commercial and cross-enterprise applications,users' functional requirements are becoming more and more complex,and it is difficult to find a single Web service to meet users' needs.Therefore,Web service composition technology emerges as The Times require and quickly becomes the focus of scholars at home and abroad.Web services composition is a technique for combining several different single services to form new services.It provides distributed software integration with a mechanism for different solutions to work together to achieve the same goal,achieving reusability of services and speeding up application development.However,due to the complexity of the service composition itself and the concurrency of the composition process,the new service after composition may not necessarily realize the service value-added,so it is very important to verify the interaction behavior of Web service composition.The reason why formal method is adopted is that formal method has a strict mathematical basis and is an important method to ensure the quality of software.It has been widely used in the specification,design,verification and other activities of computer systems and software.This paper proposes a method to verify the behavior of Web services composite interaction described by Web services business process execution language(BPEL)by using symbol model checking,and a method to verify the behavior of service composite by combining Petri net and symbol model checking.Main tasks include:1.A finite state automaton model of Web services based on message sessions is proposed,and a finite state transition diagram is used to model the BPEL process.The constructed model implements BPEL activities correspond to the finite state transition diagram one by one,and then Nu SMV code is written according to the model of the finite state transition diagram of the Web service composition,and the symbolic model checker Nu SMV is used to automatically verify the Web service composition.2.Petri net is a modeling method with intuitive graphical expression ability and rich mathematical analysis methods,but usually the analysis and verification of Petri net model is non-automated and requires researchers to have strong mathematical theory and analysis capabilities,so in order to make full use of the advantages of Petri net and avoid tedious artificial analysis,this paper puts forward the Petri net combination of symbolic model checking to verify Web service interaction method.The BPEL activity describing the Web service composition is modeled as Petri nets,and the transformation rules of Petri net and Nu SMV language are proposed,so that Nu SMV code can be written according to the Petri net model,and the Petri net model of Web service composition can be automatically verified by Nu SMV.3.Based on the two formalized methods proposed in this paper to verify the Web service composition,two application examples of Web service combination are analyzed and verified,and the whole modeling process is shown graphically.The experimental results show that the method is reliable and correct.The methods proposed in this paper realize the visualization of modeling process,automatic validation of complex Web service composite system,and verification combined with Petri net and symbol model checking. |
PDF Full Text Request