Safe Mutations of Communication Protocols

We address the correctness problem for communication protocols, which are used by automata communicating via channels. Such protocols are used in numerous real-world applications, e.g., the banking sector. The state-of-the-art approaches to verification are quite labor-intensive, and they usually have to be applied from scratch to each new protocol, even when the new protocol is obtained by only a slight modification ( mutation ) of an existing, already verified protocol. We propose a novel approach to the problem of protocol verification by describing safe mutations : a mutation (change in actors’ behavior) is safe if, when applied to a correct protocol, it produces again a correct protocol, such that the protocol’s correctness does not have to be verified anew. We formalize a communication protocol of automata as their asynchronous composition, and we formally prove that mutations based on saving local and sending actions in the involved automata are safe.