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
Finally, a detailed description of the protocol is given by the explanation of the specification itself.