Free Documentation License. Typeset in 10/12pt Computer Modern Roman by the author.

A number of issues combine to make network protocol development significantly more difficult than other areas of computer programming: problems with time, concurrency, and failures; interactions between the network protocol and its environment; and obstacles in developing the protocol over time. In order to address these issues, we introduce the Timed Abstract Protocol notation and the Austin Protocol Compiler. The Timed Abstract Protocol, or TAP, notation is a domain-specific formal language for describing asynchronous message-passing network protocols, with two execution models: an abstract ex-ecution model and a concrete execution model. The abstract execution model is suited for protocol design, comprehension, and correctness verification. The con-crete execution model is suited for protocol implementation. We show that the two models are equivalent: that a protocol interpreted under the concrete model model. The Austin Protocol Compiler, or APC, is a system that transforms