Scholarlink

<p>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 (<i>mutation</i>) of an existing, already verified protocol. We propose a novel approach to the problem of protocol verification by describing <i>safe mutations</i>: 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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

SAFE MUTATIONS OF COMMUNICATION PROTOCOLS

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年5月28日

查看全文
  • Sergei Gorlatch,
  • Natalia Garanina,
  • Igor Anureev,
  • Dmitry Kondratyev

摘要

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.