The trace specification of communications protocols

摘要

This paper describes a methodology for the formal specification of communications protocols. Specification is an important step in the successful development of software. With a specification, designers and implementors are likely to have the same expectations of the software; without a specification, costly misunderstandings often arise. 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 specifications especially important. The specification method discussed here 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 first describe the trace language and present several examples. We then describe the trace methodology, illustrated with a specification of Stenning's protocol. We summarize 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 methodology described, are a feasible technique for the formal specification of communications protocols.