Web services behavior is the key aspect to compatibility and 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 services behavioral type discipline based on extended the Martin-Lf's 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

compatibility and consistency of web services behavior are discussed.The deductions are given to show that how to verify the consistency between behavior of vendor and behavior of vendor-s.Finally

the complexity of the deduction is given.