Verification of channel passing in choreography with model checking | |
Peng, Liyang ; Cai, Chao ; Zongyan, Qiu ; Pu, Geguang | |
2009 | |
英文摘要 | 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. ?2009 IEEE.; EI; 0 |
语种 | 英语 |
出处 | EI |
内容类型 | 其他 |
源URL | [http://hdl.handle.net/20.500.11897/262994] |
专题 | 数学科学学院 |
推荐引用方式 GB/T 7714 | Peng, Liyang,Cai, Chao,Zongyan, Qiu,et al. Verification of channel passing in choreography with model checking. 2009-01-01. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论