The Austin Protocol Compiler

| The Austin Protocol Compiler, the book | News | Source | Documentation | License | APDNS | APC-examples | Authors | SourceForge project |

The Austin Protocol Compiler is a system supporting the development of asyncronous message-passing network protocols, currently focused on protocols based on UDP. The protocol compiler transforms a domain-specific language, the Timed Abstract Protocol notation, to C code and supplies a runtime environment for the Berkeley sockets interface.

The Timed Abstract Protocol notation, or TAP, is a small, simple language designed specifically for describing asynchronous message-passing network protocols with the ultimate goal of verification. TAP is based on the Abstract Protocol notation, or AP, developed by Mohamed G. Gouda, which takes a very abstract, high level approach to network protocols. Unfortunately, AP makes very strong guarantees about time, concurrency, and failure that make protocol verification easy but protocol implementation difficult.

Timed Abstract Protocol notation modifies AP slightly, preserving the ease of verification while adding the ability to express temporal behavior and moving slightly towards implementability. It is based on two execution models: a high-level, abstract model allowing protocols to be understood and verified readily, and a low-level, concrete model which makes efficient implementation possible. The relationship between these two models, which is described in detail later, is complex. However, in short, for many protocols the two models are equivalent---a protocol implemented according to the concrete model behaves the same as a protocol understandable in the abstract model.

The Austin Protocol Compiler, or APC, transforms a process described in TAP into executable code in C. The combination of the Timed Abstract Protocol notation with the Austin Protocol Compiler satisfies the three classes of network protocol development problems in the following ways:

  1. The simple domain-specific language of TAP, with its underlying formal model, addresses the intrinsic problems of protocol development through its clarity and verifiability.
  2. The clarity of the TAP language, along with the fast turn-around of a compiler, allows practical experience with a protocol while it is still in development.
  3. The formal TAP notation, with its emphasis on the protocol's details, and the ability of the compiler to create a running reference model create an environment where the compatibility problems in protocol development can be handled.

In use, the philosophy behind APC is similar to that of yacc---to provide a simple, flexible interface to complex underlying techniques. Within this philosophy, a protocol specification is written in TAP, based on the abstract execution model. APC then translates that specification into an executable system, based on the concrete execution model.

The most important requirement for APC is to correctly implement the concrete execution model of the TAP notation. Some parts of this requirement are necessarily assumptions made about the execution environment and others are implemented by the systems on which APC is based, but the major component of the requirement must be dealt with by the APC implementation. Additionally, there are two further goals for APC:

APC generates portable C code. The file containing the TAP source is filename.ap, the file filename.c contains function definitions, and the file filename.h contains the data structure definitions and function prototypes.

The Austin Protocol Compiler

The Austin Protocol Compiler has been published!

The Austin Protocol Compiler, by Tommy M. McGuire and Mohamed G. Gouda, describes APC and the TAP language and provides the formal background for development of network protocols using them. It also provides example protocols implemented using APC.

Back cover text:

The Austin Protocol Compiler presents a protocol specification language called the Timed Abstract Protocol (TAP) notation. This book will finally close the communication gap between the protocol verifiers and the protocol implementers.

The TAP notation uses two types of semantics: an abstract semantics that appeals to the protocol verifiers and a concrete semantics which appeals to the protocol implementers. The Austin Protocol Compiler illustrates that the two types of semantics of TAP are equivalent. Thus, the correctness of TAP specification of some protocol, that is established based on the abstract semantics of TAP, is maintained when this specification is implemented based on concrete semantics of TAP. The equivalence between the abstract and concrete semantics of TAP suggests the following three-step method for developing a correct implementation of a protocol in this book:

  1. Specify the protocol using the TAP notation.
  2. Verify the correctness of the specification based on the abstract semantics of TAP.
  3. Implement the specification based on the concrete semantics of TAP.

For step 3, this book introduces the Austin Protocol Compiler (APC) that takes as input, a TAP specification of some protocol, and produces as output C-code that implements this protocol based on the concrete semantics of TAP. The Austin Protocol Compiler is designed for a professional audience composed of protocol designers, verifiers, reviewers and implementers. This volume is also suitable for graduate-level students in computer science and electrical engineering.

The ISBN is 0-387-23227-3.

News

Source code

Documentation

License

GNU General Public License, Version 2

APDNS

The apdns package provides simple DNS tools implemented using the Austin Protocol Compiler. The two major components of apdns are:

apc-examples

This package provides a basic set of test programs and examples for the APC system. They are described in both Correct Implementation of Network Protocols and in The Austin Protocol Compiler.

Authors

SourceForge.net Logo