Name
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/SOCA.2009.5410263 | SOCA |
Keywords | Field | DocType |
channel passing verification,web services,choreography,channel passing,model checking,abstraction method,web service composition,global protocol,web service choreography,message passing,abstraction function,formal verification,web service | Abstraction,Model checking,Computer science,Communication channel,Choreography,Web modeling,Web service,Message passing,Distributed computing,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4244-5300-9 | 3 | 0.41 |
References | Authors | |
6 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Liyang Peng | 1 | 19 | 2.50 |
| Chao Cai | 2 | 145 | 8.48 |
| Zongyan Qiu | 3 | 436 | 41.04 |
| Geguang Pu | 4 | 602 | 57.89 |