@inproceedings{e91c555cc7e04a6c948192183f778390,
title = "Verification of channel passing in choreography with model checking",
abstract = "A web service choreography describes a global protocol of interactions among a set of cooperating services. For the dynamic composition, changing interconnections by channel passing between services is necessary. In this paper we use model checking technique for the verifying problems related to channel passing in choreography. We develop a framework: for each kind of property to be verified, we define an abstraction function based on it, which map each basic interaction into a pair of pre- and post-conditions, then propose a compositional approach to translate choreographies into models for model checkers. A number of examples are presented to show how the verification is carried out.",
keywords = "Abstraction method, Channel passing, Choreography, Model checking, Web service composition",
author = "Liyang Peng and Chao Cai and Qiu Zongyan and Geguang Pu",
year = "2009",
doi = "10.1109/SOCA.2009.5410263",
language = "英语",
isbn = "9781424452996",
series = "IEEE International Conference on Service-Oriented Computing and Applications, SOCA' 09",
pages = "286--290",
booktitle = "IEEE International Conference on Service-Oriented Computing and Applications, SOCA' 09",
note = "IEEE International Conference on Service-Oriented Computing and Applications, SOCA' 09 ; Conference date: 14-12-2009 Through 15-12-2009",
}