Towards hierarchical modeling and analysis of web services choreography

Web services choreography as an important approach of composing web services describes the global model of service interactions among a set of participants. Modern software design paradigms promote hierarchy as one of the key constructs for structuring complex specifications. In development of complex service-oriented systems, hierarchical composition in which a composed service could also be composed into a high level system model is a great approach for system modeling, and behavioural equivalence which checks whether two choreographies in different levels describe essentially the same behaviour is an important aspect of system verification. This paper proposes a formal modeling and analysis approach for hierarchical web services choreographies. A formal language Chor which originates from WS-CDL describes dynamic behaviour of choreographies and a novel bisimulation is used for analyzing behavioural equivalence of Chor language. We introduce a hierarchical model for describing and analyzing complex choreographies. Abstract choreographies can be refined to detailed models and external and observable behaviour be preserved equivalently. Our approach can also be extended to formally analyze hierarchical and global interaction models for general concurrent systems.