The Calculus of Handshake Configurations
| 详细信息 | 推荐本文 | |
- 作者：Luca Fossati ; Daniele Varacca
- 关键词：Handshake protocols ; Petri nets ; process calculus ; types
- 刊名：Lecture Notes in Computer Science
- 出版时间：2009
- 出版年：2009
- 期刊代码：99_0302-9743
- 类别：cp
- 卷：5504
- 期：1
- 页码：227-241
- 数据来源：sp
摘要
Handshake protocols are asynchronous protocols that enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. We propose a concurrent process calculus for handshake protocols. This calculus uses two mechanisms of synchronization: rendez-vous communication 脿 la CCS, and shared resource usage. To enforce the handshake discipline, the calculus is endowed with a typing system. We provide an LTS semantics of the calculus and show that typed processes denote handshake protocols. We give the calculus another semantics in terms of a special kind of Petri nets called handshake Petri nets. We show that this semantics is complete and fully abstract with respect to weak bisimilarity.