![Sample our Bioscience journals, sign in here to start your access, Latest two full volumes FREE to you for 14 days]({"type":"image" , "src" : "/sda/5925/TOC-Subject-Sample-2021-Bioscience.jpg"})
Abstract
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.
Acknowledgements
Yongxin Zhao is partially supported by NSFC Project No. 91118007. Hao Xiao is partially supported by NSFC Projects Nos. 61061130541 and 61021004. Zheng Wang is partially supported by 973 Project No. 2011CB302904. Geguang Pu is partially supported by Shanghai Knowledge Service Platform for Trustworthy Internet of Things No. ZF1213 and Civil Aerospace Project 125.
Notes
1. In this paper, the communication mechanisms are restricted to be synchronous, however, the restriction is not critical; the asynchronous mechanism can be modelled by the synchronous one and time constructor.
2. In order to distinguish the transitions between the execution model and the CSP# model, we use the notations →# and →t # to describe the transitions in the CSP# model.