Formalizing Compatibility and Substitutability in Communication Protocols Using I/O-Constraint Automata

Abstract. A communication protocol consists of a sequence of messages used by peer entities to communicate. Each entity in a network is equipped by at least one protocol stack. Due to the need for on the fly reconfiguration of protocol stack in future communication and computation devices, formalizing substitutability and compatibility of protocol entities are important in correctness assessment of dynamic reconfiguration. In this paper, we extend Constraint Automata and propose I/OConstraint Automata to model behavior of protocols and propose enough formalism for substitutability and compatibility relations between protocols. We introduce input-blocking property of communication protocols, and show that in the context of communication protocols simulation relation is not strong enough for notion of substitutability. We show the relation between substitutability and compatibility to reason about the correctness in substitution of a protocol with a new one.

• Type: Conference
• Year: 2007
• Where: FSEN
• Authors: Mahdi Niamanesh, Rasool Jalili
• Keywords: Communication Protocols, Communication Protocols Simulation, FSEN 2007, Protocol Stack