需要一个社区：在当前规范与形式规范之间的鸿沟
网络与互联网体系结构
2025-09-17 v1 形式语言与自动机理论
摘要
形式规范对网络协议的设计者和用户都有诸多好处。它们提供清晰、无歧义的表示，对于文档和测试都有用。它们可以帮助揭示关于协议 "是什么"的不同观点，并识别需要进一步工作以解决歧义或内部不一致性的领域。它们还为形式推理提供了基础，使得可能在所有输入和每个环境中建立重要的安全和正确性保证。尽管有这些优势，形式方法在今天的网络协议设计、实现和验证中并不广泛使用。相反，Internet 协议通常描述在非正式文档中，例如 IETF 请求注释 (RFC) 或 IEEE 标准。这些文档主要由冗长的文字描述、伪代码、标题描述、状态机图和用于互操作性测试的参考实现组成。因此，尽管 RFC 和参考实现最初仅旨在帮助指导协议设计者使用的社交过程，但它们已演变为互联网社区拥有的最接近形式规范的东西。在本文中，我们讨论了规范在网络和形式方法社区中扮演的不同角色。我们随后概述了正式指定协议的潜在好处，呈现了来自几个最近成功案例的亮点。最后，我们确定了两种社区对形式规范理解的关键差异，并提出了可能的策略来弥合这些差距。
引用
@article{arxiv.2509.13208,
title = {It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols},
author = {David Basin and Nate Foster and Kenneth L. McMillan and Kedar S. Namjoshi and Cristina Nita-Rotaru and Jonathan M. Smith and Pamela Zave and Lenore D. Zuck},
journal= {arXiv preprint arXiv:2509.13208},
year = {2025}
}