topic.netsem.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"netsem" -ob topic.netsem.bib sewellbib2.bib}}

@techreport{SSW01b,
  author = {Andrei Serjantov and Peter Sewell and Keith Wansbrough},
  title = {The {UDP} Calculus: Rigorous Semantics for Real Networking},
  institution = {Computer Laboratory, University of Cambridge},
  year = {2001},
  optkey = {},
  opttype = {},
  number = {UCAM-CL-TR-515},
  optaddress = {},
  month = jul,
  note = {iv+70pp. },
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/udp-long.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/udp-long.ps},
  url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-515.html},
  abstract = {Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP, etc.), concurrency, packet loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle protability issues. Moreover, the behavioural properties of operating systems and the network are not well documented.

A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what has been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs that use these protocols.

In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP, including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language, but can be used with any language equipped with an operational semantics for system calls – here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.
},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{SSW01a,
  author = {Andrei Serjantov and Peter Sewell and Keith Wansbrough},
  title = {The {UDP} Calculus: Rigorous Semantics for Real Networking},
  conf = {TACS 2001},
  booktitle = {Proceedings of  Theoretical Aspects of Computer Software (Sendai), LNCS 2215},
  optcrossref = {},
  optkey = {},
  pages = {535--559},
  year = {2001},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = oct,
  optorganization = {},
  optpublisher = {},
  note = {},
  optannote = {},
  url = {https://doi.org/10.1007/3-540-45500-0_27},
  doi = {10.1007/3-540-45500-0_27},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/Netsem/udp-short.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/udp-short.ps},
  abstract = {Network programming is notoriously hard to understand:
one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc),
concurrency, packet loss, host failure, timeouts, the complex sockets interface 
to the protocols, and subtle portability issues. Moreover, the behavioural prope
rties of operating systems and the network are not well
documented.

A few of these issues have been addressed in the process calculus and
distributed algorithm communities, but there remains a wide gulf between what ha
s been captured in semantic models and what is required
for a precise understanding of the behaviour of practical distributed programs t
hat use these protocols.

In this paper we demonstrate (in a preliminary way) that the gulf can
be bridged. We give an operational model for socket programming with
a substantial fraction of UDP and ICMP, including loss and failure. The
model has been validated by experiment against actual systems. It is not
tied to a particular programming language, but can be used with any
language equipped with an operational semantics for system calls - here
we give such a language binding for an OCaml fragment. We illustrate
the model with a few small network programs.
},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{WNSS01,
  author = {Keith Wansbrough and Michael Norrish and Peter Sewell and Andrei Serjantov},
  title = {Timing {UDP}: mechanized semantics for sockets, threads and failures},
  conf = {ESOP 2002},
  booktitle = {Proceedings of the 11th European Symposium on Programming (Grenoble), LNCS 2305},
  optcrossref = {},
  optkey = {},
  pages = {278--294},
  year = {2002},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = apr,
  optorganization = {},
  optpublisher = {},
  note = {},
  optannote = {},
  url = {https://doi.org/10.1007/3-540-45927-8_20},
  doi = {10.1007/3-540-45927-8_20},
  ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/timing-udp-a4.ps},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/timing-udp-a4.pdf},
  abstract = {This paper studies the semantics of failure in distributed
programming. We present a semantic model for distributed programs
that use the standard sockets interface; it covers message loss, host failure
and temporary disconnection, and supports reasoning about distributed
infrastructure. We consider interaction via the UDP and ICMP protocols.
To do this, it has been necessary to: $\bullet$ construct an experimentallyvalidated
post-hoc specification of the UDP/ICMP sockets interface;
$\bullet$ develop a timed operational semantics with threads, as such programs
are typically multithreaded and depend on timeouts; $\bullet$ model the behaviour
of partial systems, making explicit the interactions that the infrastructure
offers to applications; $\bullet$ integrate the above with semantics
for an executable fragment of a programming language (OCaml) with OS
library primitives; and $\bullet$ use tool support to manage complexity, mechanizing
the model with the HOL theorem prover. We illustrate the whole
with a module providing na¨ıve heartbeat failure detection.},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{NSW02,
  author = {Michael Norrish and Peter Sewell and Keith Wansbrough},
  title = {Rigour is good for you, and feasible: reflections on formal treatments of {C} and {UDP} sockets. },
  conf = {SIGOPS EW 2002},
  booktitle = {Proceedings of the 10th ACM SIGOPS European Workshop (Saint-Emilion)},
  optcrossref = {},
  optkey = {},
  pages = {49--53},
  year = {2002},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = sep,
  optorganization = {},
  optpublisher = {},
  note = {},
  optannote = {},
  url = {http://doi.acm.org/10.1145/1133373.1133383},
  doi = {10.1145/1133373.1133383},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/Netsem/sigops-ew2002.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/sigops-ew2002.ps},
  abstract = {We summarise two projects that formalised complex real
world systems: UDP and its sockets API, and the C programming language. We describe their goals and the techniques used in both. We conclude by discussing how such
techniques might be applied to other system software and
by describing the benefits this may bring.},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@techreport{TCP:tr,
  optkey = {},
  author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {{TCP}, {UDP}, and {S}ockets: rigorous and experimentally-validated
behavioural specification. {V}olume 1: Overview},
  institution = {Computer Laboratory, University of Cambridge},
  number = {UCAM-CL-TR-624},
  note = {88pp},
  optnote = {Available at \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/}},
  month = mar,
  year = {2005},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/tr.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/tr.ps},
  url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-624.html},
  abstract = {
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface interactions of a host, using operational semantics in the higher-order logic of the HOL automated proof assistant. The specification is detailed, covering almost all the information of the real-world communications: it is in terms of individual TCP segments and UDP datagrams, though it abstracts from the internals of IP. It has broad coverage, dealing with arbitrary API call sequences and incoming messages, not just some well-behaved usage. It is also accurate, closely based on the de facto standard of (three of) the widely-deployed implementations. To ensure this we have adopted a novel experimental semantics approach, developing test generation tools and symbolic higher-order-logic model checking techniques that let us validate the specification directly against several thousand traces captured from the implementations.

The resulting specification, which is annotated for the non-HOL-specialist reader, may be useful as an informal reference for TCP/IP stack implementors and Sockets API users, supplementing the existing informal standards and texts. It can also provide a basis for high-fidelity automated testing of future implementations, and a basis for design and formal proof of higher-level communication layers. More generally, the work demonstrates that it is feasible to carry out similar rigorous specification work at design-time for new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to protocol specifications that are both unambiguous and clear, and to high-quality implementations that can be tested directly against those specifications.

This document (Volume 1) gives an overview of the project, discussing the goals and techniques and giving an introduction to the specification. The specification itself is given in the companion Volume 2 (UCAM-CL-TR-625), which is automatically typeset from the (extensively annotated) HOL source. As far as possible we have tried to make the work accessible to four groups of intended readers: workers in networking (implementors of TCP/IP stacks, and designers of new protocols); in distributed systems (implementors of software above the Sockets API); in distributed algorithms (for whom this may make it possible to prove properties about executable implementations of those algorithms); and in semantics and automated reasoning.},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@techreport{TCP:spec,
  optkey = {},
  author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {{TCP}, {UDP}, and {S}ockets: rigorous and experimentally-validated
behavioural specification. {V}olume 2: The
Specification.},
  institution = {Computer Laboratory, University of Cambridge},
  number = {UCAM-CL-TR-625},
  note = {386pp},
  optnote = { Available at \url{http://www.cl.cam.ac.uk/users/pes20/Netsem/}},
  month = mar,
  year = {2005},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/alldoc.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/alldoc.ps},
  url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-625.html},
  abstract = {See Volume 1 (UCAM-CL-TR-624).},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{TCP:paper,
  optkey = {},
  author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {Rigorous specification and conformance testing techniques for network protocols, as applied to {TCP}, {UDP}, and {S}ockets},
  year = {2005},
  optnote = {12pp},
  optcrossref = {},
  optkey = {},
  conf = {SIGCOMM 2005},
  booktitle = {Proceedings of  the ACM Conference on Computer Communications (Philadelphia), \emph{published as Vol.~35, No.~4 of} {{Computer Communication Review}}},
  pages = {265--276},
  optyear = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = aug,
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  url = {http://doi.acm.org/10.1145/1080091.1080123},
  doi = {10.1145/1080091.1080123},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/paper.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/paper.ps},
  abstract = {
Network protocols are hard to implement correctly. Despite the 
existence of RFCs and other standards, implementations often 
have subtle differences and bugs. One reason for this is that the 
specifications are typically informal, and hence inevitably contain 
ambiguities. Conformance testing against such specifications is 
challenging. 

In this paper we present a practical technique for rigorous 
protocol specification that supports specification-based testing. We 
        have applied it to TCP, UDP, and the Sockets API, developing 
        a detailed ‘post-hoc’ specification that accurately reflects the 
                behaviour of several existing implementations (FreeBSD 4.6, 
                Linux 2.4.20-8, and Windows XP SP1). The development process 
                uncovered a number of differences between and infelicities in these 
                implementations. 

                Our experience shows for the first time that rigorous specification 
                    is feasible for protocols as complex as TCP. 
                    We argue 
                    that the technique is also applicable ‘pre-hoc’, in the design 
                        phase of new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to 
                          protocol specifications that are both unambiguous and clear, and 
                            to high-quality implementations that can be tested directly against 
                            those specifications. 

},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{TCP:techpaper,
  optkey = {},
  author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {Engineering with Logic: {HOL} Specification and Symbolic-Evaluation Testing for {TCP} Implementations},
  year = {2006},
  pages = {55--66},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2006},
  booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston)},
  optpages = {},
  optyear = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = jan,
  optorganization = {},
  optpublisher = {},
  optnote = {To appear.},
  optannote = {},
  url = {http://doi.acm.org/10.1145/1111037.1111043},
  doi = {10.1145/1111037.1111043},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/Netsem/tech-paper.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/Netsem/tech-paper.ps},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{BDJRS06,
  author = {Adam Biltcliffe and Michael Dales and Sam Jansen and Thomas Ridge and Peter Sewell},
  title = {Rigorous Protocol Design in Practice: An Optical Packet-Switch {MAC} in {HOL}},
  optcrossref = {},
  optkey = {},
  conf = {ICNP 2006},
  booktitle = {Proceedings of  the 14th IEEE International Conference on Network Protocols (Santa Barbara)},
  optpages = {},
  year = {2006},
  pages = {117--126},
  numpages = {10},
  opturl = {http://dx.doi.org/10.1109/ICNP.2006.320205},
  url = {https://doi.org/10.1109/ICNP.2006.320205},
  doi = {10.1109/ICNP.2006.320205},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = nov,
  optorganization = {},
  optpublisher = {},
  optannote = {},
  note = {See also the  SWIFT MAC Protocol: HOL Specification at \url{http://www.cl.cam.ac.uk/~pes20/optical/spec.pdf}},
  pdf = {http://www.cl.cam.ac.uk/~pes20/optical/root.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/optical/root.ps},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
  abstract = {
This paper reports on an experiment in network
protocol design: we use novel rigorous techniques in the design
process of a new protocol, in a close collaboration between
systems and theory researchers.

The protocol is a Media Access Control (MAC) protocol for
the SWIFT optical network, which uses optical switching and
wavelength striping to provide very high bandwidth packet-switched interconnects. The use of optical switching (and the
lack of optical buffering) means that the protocol must control
the switch within hard timing constraints.

We use higher-order logic to express the protocol design,
in the general-purpose HOL automated proof assistant. The specification is thus completely precise, but still concise, readable, and without accidental overspecification. Further, we test
conformance between the specification and two implementations
of the protocol: an NS-2 simulation model and the VHDL code of
the network hardware. This involves: (1) proving, within HOL,
that the specification is equivalent to an algorithmically-checkable
version; (2) using automatic code-extraction to generate a testing
oracle; and (3) applying that oracle to traces of the implementation.

This design-time use of rigorous methods has resulted in a
protocol that is better specified and more correct than it would
otherwise be, with relatively little effort.
},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@inproceedings{RNS08,
  author = {Tom Ridge and Michael Norrish and Peter Sewell},
  title = {A rigorous approach to networking: {TCP}, from implementation to protocol to service},
  optcrossref = {},
  optkey = {},
  conf = {FM 2008},
  booktitle = {Proceedings of the 15th International Symposium on Formal Methods (Turku, Finland), LNCS 5014},
  pages = {294--309},
  year = 2008,
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = may,
  optorganization = {},
  optpublisher = {},
  optnote = {To appear},
  optannote = {},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
  url = {https://doi.org/10.1007/978-3-540-68237-0_21},
  doi = {10.1007/978-3-540-68237-0_21},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/stream_spec.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/stream_spec.ps},
  abstract = {Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part this is because the scale and complexity of these protocols makes them challenging targets for formalization.

In this paper we show how these difficulties can be addressed. We develop a high-level specification for TCP and the Sockets API, expressed in the HOL proof assistant, describing the byte-stream service that TCP provides to users. This complements our previous low-level specification of the protocol internals, and makes it possible for the first time to state what it means for TCP to be correct: that the protocol implements the service. We define a precise abstraction function between the models and validate it by testing, using verified testing infrastructure within HOL. This is a pragmatic alternative to full proof, providing reasonable confidence at a relatively low entry cost.

Together with our previous validation of the low-level model, this shows how one can rigorously tie together concrete implementations, low-level protocol models, and specifications of the services they claim to provide, dealing with the complexity of real-world protocols throughout.},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@techreport{UCAM-CL-TR-742,
  author = {Ridge, Thomas and Norrish, Michael and Sewell, Peter},
  title = {{TCP, UDP, and Sockets: Volume 3: The Service-level
         	   Specification}},
  year = 2009,
  month = feb,
  pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-742.pdf},
  institution = {University of Cambridge, Computer Laboratory},
  number = {UCAM-CL-TR-742},
  note = {305pp},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@misc{udp-model,
  optkey = {SWN01},
  author = {Michael Norrish and Andrei Serjantov and Peter Sewell and Keith Wansbrough},
  title = {Timing {UDP}: The {HOL} Model},
  opthowpublished = {},
  month = jul,
  year = {2001},
  note = {\url{http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html}},
  url = {http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html},
  optannote = {},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@misc{netsem04a,
  optkey = {},
  author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and Peter Sewell and Keith
Wansbrough},
  title = {The {TCP} Specification: A Quick Introduction},
  opthowpublished = {},
  optmonth = {},
  year = {2004},
  optnote = {},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/quickstart.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/quickstart.ps},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@misc{TCP:poster,
  optkey = {},
  author = {Steven Bishop and Matthew Fairbairn and Michael Norrish and
Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {An approximation to the real TCP state diagram},
  opthowpublished = {},
  month = mar,
  year = {2005},
  note = {This is a poster with a version of the "TCP state diagram" extracted from the specification. It is rather more complete than the usual diagram, but is still a very abstract and simplified view of the state space of our specification. It is intended to be printed at A1 size or bigger.},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/poster.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/Netsem/poster.ps},
  topic = {netsem},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem}
}

@article{tcp3draft,
  optkey = {},
  author = {Steve Bishop and Matthew Fairbairn and Hannes Mehnert and Michael Norrish and Tom Ridge and Peter Sewell and Michael Smith and Keith Wansbrough},
  title = {Engineering with Logic: Rigorous Test-Oracle Specification and Validation for {TCP/IP} and the {Sockets API}},
  journal = {J. ACM},
  opthowpublished = {},
  optmonth = {},
  issue_date = {December 2018},
  volume = {66},
  number = {1},
  month = dec,
  year = {2018},
  issn = {0004-5411},
  pages = {1:1--1:77},
  articleno = {1},
  numpages = {77},
  url = {http://doi.acm.org/10.1145/3243650},
  doi = {10.1145/3243650},
  acmid = {3243650},
  publisher = {ACM},
  optaddress = {New York, NY, USA},
  optnote = {Accepted for publication 2018-08},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf},
  project = {http://www.cl.cam.ac.uk/~pes20/Netsem/index.html},
  optrecent = {true},
  topic = {netsem},
  abstract = {
Conventional computer engineering relies on test-and-debug development
processes, with the behaviour of common interfaces described (at best)
with prose specification documents.  But prose specifications cannot be used in
test-and-debug development in any automated way, and prose is a poor
medium for expressing complex (and loose) specifications. 

The TCP/IP protocols and Sockets API are a good example of this:
they play a vital role in modern communication and computation, and
interoperability between implementations is essential.  But what
exactly they are is surprisingly obscure: their original development
focussed on ``rough consensus and running code'', augmented by prose
RFC specifications that do not precisely define what it means for an
implementation to be correct.  Ultimately, the actual standard is the
de facto one of the common implementations, including, for example,
the 15\,000--20\,000 lines of the BSD implementation --- optimised and
multithreaded C code, time-dependent, with asynchronous event
handlers, intertwined with the operating system, and
security-critical.

This paper reports on work done in the \emph{Netsem} project to
develop lightweight mathematically rigorous techniques that can be
applied to such systems: to specify their behaviour precisely (but
loosely enough to permit the required implementation variation) and to
test whether these specifications and the implementations correspond,
with specifications that are \emph{executable as test oracles}.
We developed post-hoc specifications of TCP, UDP, and the Sockets API, both of
the service that they provide to applications (in terms of TCP
bidirectional stream connections), and of the internal operation of
the protocol (in terms of TCP segments and UDP datagrams), together
with a testable abstraction function relating the two.  These specifications
are rigorous, detailed, readable, with broad coverage, and are rather
accurate.  Working within a general-purpose proof assistant (HOL4), we
developed \emph{language idioms} (within higher-order logic) in which
to write the specifications: operational semantics with
nondeterminism, time, system calls, monadic relational programming,
etc.  We followed an \emph{experimental semantics} approach,
validating the specifications 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 \emph{symbolic model
  checker} programmed above HOL4.

Having demonstrated that our logic-based engineering techniques
suffice for handling real-world protocols, we argue that similar
techniques could be applied to future critical software infrastructure
at design time, leading to cleaner designs and (via
specification-based testing) more robust and predictable
implementations.  In cases where specification looseness can be
controlled, this should be possible with lightweight techniques,
without the need for a general-purpose proof assistant, at relatively
little cost.
}
}