Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations

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 ...

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
• Keywords: Future Critical Software, General Terms Documentation, General-purpose Proof Assistant, POPL 2006, Programming Languages