The Calculus of Handshake Configurations

摘要

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 a la CCS, and shared resource usage. To enforce the handshake discipline, the calculus is endowed with a typing system.rnWe 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.