Verifying Consistency of Web Services Behavior Using Type Theory

Web services behavior is the key aspect to consistency of Web services, which can ensure correctness and reliability in Web services choreography. But few methods can conduct the trade-off between expressiveness and amenability of efficient verification, this paper gives a better answer to solve the problem. It constructs service-behavioral type discipline based on extended the Martin-Lofpsilas Type Theory (for short, MTT) which supports a type-theoretic formulation of services behavior structured patterns, so that services behavior in a distributed system can be verified by type checking. Then, the type rules for subtype, duality, and consistency of Web services behavior are discussed. The deductions are gave to show that how to verify the consistency between behavior of vendor and behavior of vendor-s.