The semantics and verification of timed service choreography

As a service composition and coordination language, the service choreography gives the global and neutral view on the collaboration among a collection of highly distributed services involving multiple different organizations or heterogeneous independent processes. In this paper, we extend the service choreography by introducing the explicit time activity, which can be used to specify and reason about the timed behaviour of Web service choreography. Then we explore an execution model for the proposed timed service choreography which possesses several novel features, such as timed activity, choreography composition, exception handling and finalization. Furthermore, a set of mapping rules is elaborately designed to translate the timed choreography into communicating sequential programs processes, thus the corresponding simulation and verification of Web services choreographies with timing restrictions can be carried out in the model checker process analysis toolkit. The case study shows that our approach is both effective and practical.