Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations
复制标题
逻辑工程：TCP 实现的 HOL 规范和符号评估测试
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Keith Wansbrough
中科院分区：
文献类型：
--
作者：
S. Bishop;M. Fairbairn;Michael Norrish;Peter Sewell;Michael Smith;Keith Wansbrough
TCP/IP协议和Sockets API是现代计算的基础，但它们的语义在历史上非常复杂且定义不清。真实的标准是事实上的通用实现之一，例如，包括BSD实现中的15，000 - 20，000行C语言。严格地处理这些代码体的行为是具有挑战性的。我们最近开发了一个TCP、UDP和Sockets的事后规范，该规范严格、详细、可读、覆盖面广，并且非常准确。在本文中，我们描述了所需的新技术。在一个通用的证明助理（HOL）工作，我们开发了语言习惯用法（在高阶逻辑中）在其中编写规范：操作语义与非确定性，时间，系统调用，一元关系编程等，我们遵循实验语义的方法，根据从三个实现（FreeBSD、Linux和WinXP）捕获的数千条跟踪来验证规范。它们之间的许多差异被确定，以及一些错误。我们建议类似的逻辑工程技术可以应用于未来的关键软件基础设施在设计时，导致更干净的设计和（通过基于规范的测试，使用类似的检查）更可预测的实现。
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common implementations, including, for example, the 15,000--20,000 lines of C in the BSD implementation. Dealing rigorously with the behaviour of such bodies of code is challenging.We have recently developed a post-hoc specification of TCP, UDP, and Sockets that is rigorous, detailed, readable, has broad coverage, and is remarkably accurate. In this paper we describe the novel techniques that were required.Working within a general-purpose proof assistant (HOL), we developed language idioms (within higher-order logic) in which to write the specification: operational semantics with nondeterminism, time, system calls, monadic relational programming, etc. We followed an experimental semantics approach, validating the specification against several thousand traces captured from three implementations (FreeBSD, Linux, and WinXP). Many differences between these were identified, and a number of bugs. Validation was done using a special-purpose symbolic model checker programmed above HOL.We suggest that similar logic engineering techniques could be applied to future critical software infrastructure at design time, leading to cleaner designs and (via specification-based testing using a similar checker) more predictable implementations.