Towards the Verification of Services Collaboration

Assuring the consistency between collaborative services is a challenge problem in service oriented architecture. In this paper, we propose an approach to verifying the consistency of collaborative services based upon model checking. We first introduce an Extended UML Sequence Diagram for modeling dynamic behavior of collaborative service combining with UML State Chart Diagram. And then we define Collaboration-Contracts and obtain the verification model from the dynamic behavior models. Finally, wean automatically verify the consistency of collaborative services in behavior models by using an integrated SPIN-binding modeling tool Trustable MDA we developed to, In addition, a user-friendly service simulator is provided to locate the position of inconsistency.