Protocol Compatibility Verification for Web Services Interaction

In this paper, a formal service behavior model called service-net based on colored Petri net (CP-Net) has been presented. Service-Net can be used to describe not only the control dependency and data dependency among inner operations of Web services, but also the message interactions of services with outer environments as an independent communication system. The correctness of interaction protocol is the key to assuring the success of services interactions. Based on Service-Net of services participating the interaction, the construct of the formal protocol model of services interaction called has further defined. Finally, the correctness justification criteria of protocol model as well as the corresponding verification method based on CP-Net theory has been given.