Towards The Verification Of Services Collaboration Based On Model Checking

Recently Service Oriented Architecture (SOA) has gained more and more attentions as a very perspective software development technique. SOA's feature of loosely coupled promises rapid services composition and dynamic reconfiguration, but it also challenges the consistency and reliability of systems. Therefore, there has been increasing interest on the verification of the consistency and reliability of services collaboration on model level, which can reduce the risk of SOA application development and save a lot of resources.Unified Modeling Language (UML) is widely used as a representation of an analysis and design method for object orientation. UML is a unified, powerful and visual language and is also easy to use. Its advantages make it become a core technique in the model driven software development process. But since UML lacks formal semantics, it is hard to check whether the design specification in UML satisfies the requirement of the system.After studying the concepts of services collaboration and relative verification techniques, this paper proposes an approach to verifying the consistency among dynamic collaborative services based on SPIN.At first, we extend UML Sequence Diagram with state attribute to Extended Sequence Diagram (ESD). Attribute of Enter State is added to messages and the extension has enhanced the express power of sequence diagram in describing system dynamic behaviors. Secondly, based on the analysis of services collaboration and semantics of ESD, we formally describe the concept of Collaboration-Contracts (CC) and define the consistency among dynamic behaviors of services in system. This will support the formalism for collaboration protocols of services. Thirdly, we translate UML State Diagram, which models the dynamic behavior of the system, to Promela (a model language accepted by model checker SPIN) according to the mapping rules. And the Collaboration-Contracts modeled by ESD are mapped to LTL expressions. We insure the consistency among dynamic collaborative services in system by verifying if the dynamic behaviors in Promela satisfy the Collaboration-Contracts in the format of LTL expressions by SPIN. Finally, we design and implement the integrated development environment for modeling and verification tMDA (Trustable Model Driven Architecture) on the basis of the work we introduced above. Using tMDA, we model and verify the interlocking station stimulation system in track traffic.