  We present a rigorous framework for automatically testing application-layer
protocols. The key innovation is a domain-specific embedded language for
writing nondeterministic models of the behavior of networked servers. These
models are defined in Gallina, the language of the Coq interactive theorem
prover, supporting a smooth transition from testing to formal verification.
  Given a server model, we show how to automatically derive a testing program
that probes the server for unexpected behaviors. We address the uncertainties
caused by both the server's internal choices and the network delaying messages
nondeterministically. The derived tester accepts server implementations whose
possible behaviors are a subset of those allowed by the nondeterministic model.
  We demonstrate the effectiveness of this framework by using it to specify and
test a fragment of HTTP/1.1, showing that the automatically derived tester can
capture RFC violations in buggy server implementations, including the latest
versions of Apache and Nginx.
