Paper Info
Title
Reasoning about Channel Passing in Choreography
Abstract
Web services choreography describes global models of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel(s) used in the interaction, otherwise the execution will get stuck. Because of dynamic composition, the initial channel set on each participant is often insufficient to meet the requirements. It is the responsibility of the participants to pass required channels owned (known) by one to some others. Since a choreography may involve many participants and complex channel constraints, it is hard for designers to specify channel passing in a choreography exactly as required. In this paper, we address the problem of checking whether a choreography lacks channels or has redundant channels, and how to automatically generate channel passing based on interaction flows of the choreography in the case of channel absence. Concretely, we propose a small language Chorc named for a channel interaction sub-language for modeling the channel passing aspect of choreography. Based on the formal operational semantics of Chorc, the algorithms for static checking choreography and generating channel passing are studied as well.
Year
DOI
Venue
2008
10.1109/TASE.2008.19
Nanjing
Keywords
Field
DocType
finite automaton,channel passing,early eighty,model checking,flourishing research area,qualitative property,initial focus,web service,operational semantics,software engineering,application software,process control,informatics,web services,computer science,formal specification,protocols
Information system,Operational semantics,Programming language,Computer science,Communication channel,Formal specification,Choreography,Web service,Static checking
Conference
ISBN
Citations 
PageRank 
978-0-7695-3249-3
8
0.62
References 
Authors
21
5
Name
Order
Citations
PageRank
Hongli Yang119114.80
Chao Cai21458.48
Liyang Peng3192.50
Xiangpeng Zhao435320.67
Zongyan Qiu543641.04