Formally Specifying a Communications Protocol Using the Trace Assertion Method

Mr. Francois Courtois

Dr. David Lorge Parnas

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1


This paper is an application of the trace assertion method to a telecommunications protocol. The protocol used as an example is the Medium Access control (MAC) protocol of the Fiber Distributed Data Interface (FDDI). A brief description of this network and its MAC protocol are given.

Although the trace assertion method was originally designed for software programs, we attempt to write a formal specification of the protocol's behaviour. Minor additions to the method were needed: we explain how to generate "internal" events and introduce a notation for describing relations between input variables.

Finally, a detailed description of the protocol is given by the explanation of the specification itself.