Formally Specifying a Communications Protocol Using the Trace Assertion Method

Mr. Francois Courtois

Dr. David Lorge Parnas
(parnas@mcmaster.ca)

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


Abstract

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.