Verifying Consistency of Web Services Behavior

Consistency of Web services behavior is the key to ensure correctness and reliability of Web services choreography technology. In the paper, we introduce Martin-Lof type theory (MTT) and extend it to have a strong expressive capacity to describe formally Web services behavior. Based on this idea behind MTT, the paper applies extended-MTT to formally describe Web services behavior. Then, the rules of consistency are proposed based on combination of extended-MTT and type discipline. Next, the procedures of proofs are given that verify the consistency between behavior of vendor and behavior of vendor-s. In one word, our way is a suitable trade-off between expressiveness and amenability to efficiently verify.