A Petri Net Model of HandShake Protocols

• Main Authors: Fossati, Luca, Varacca, Daniele
• Other Authors: Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica Torino, Università degli studi di Torino = University of Turin (UNITO)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2008
• Subjects: Handshake protocol; Petri nets; asynchronous communications; delay-insensitivity; transmission interference; [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]; Iceland
• Online Access: https://hal.science/hal-00496907

International audience We propose a Petri net model of handshake protocols. These are asynchronous communication protocols which enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. We introduce the notion of \emph{handshake Petri net}, a Petri net with a specific external interface. We show that the set of observable \emph{quiescent} traces generated by such a net captures the properties defining a handshake protocol. Conversely we show that for any handshake protocol we can construct a corresponding net. We also study different subclasses of the model. Many examples are provided.