TRACE SPECIFICATION OF COMMUNICATIONS PROTOCOLS (SOFTWARE ENGINEERING, FORMAL SPECIFICATION)

This dissertation describes a methodology for the formal specification of communications protocols. Specification is an important step in the successful development of computer software. Further, it is important that these specifications be precise. With such a specification, designers and implementors are likely to have the same expectations of the software; without a specification, costly misunderstandings often arise.;The specification method chosen for this dissertation is a modified version of traces, developed by Parnas and Bartussek. Traces were originally developed as a general technique for software specification. Until now, only trace specifications of small, simple modules had been attempted, and no trace specifications of communications protocols existed. We discuss an extension made to traces to handle communications protocol specification. We then describe the trace methodology comprised of heuristics which make the specification of complex communications protocols intellectually manageable. We describe our experience in using the methodology to write specifications of major portions of two commercial standards: the Advanced Data Communications Control Protocol (ADCCP) and the Internet Protocol (IP).;Finally, we conclude that traces, using the extension and methodology described herein, are a feasible technique for the formal specification of communications protocols, and that traces explicitly address deficiencies in methods currently in use.;Communications protocol software offers special specification problems. Typically, such software connects computers that are widely distributed geographically and differ in model, manufacturer, and operating system. Thus, for communications protocol software, misunderstandings are particularly likely, making precise specification especially important. Formal specifications, written in a language with formally defined syntax and semantics, support precise specification and are also suitable for verification. Various techniques have been proposed for the formal specification of communications protocols, each with certain drawbacks.