Formalizing compatibility and substitutability in communication protocols using I/O-constraint automata
Mahdi Niamanesh, Rasool Jalili · 2007
Abstract. A communication protocol consists of a sequence of mes-sages 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 compu-tation devices, formalizing substitutability and compatibility of protocol entities are important in correctness assessment of dynamic reconfigura-tion. In this paper, we extend Constraint Automata and propose I/O-Constraint Automata to model behavior of protocols and propose enough formalism for substitutability and compatibility relations between proto-cols. We introduce input-blocking property of communication protocols, and show that in the context of communication protocols simulation re-lation 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. 1