Modeling a transport layer protocol using first-order logic

ABSTRACT

We use a hybrid model based on the first-order logic to specify and verify a transport layer protocol. In this model we specify a protocol as a set of state machines. Time expressions are used to describe the temporal relations of transitions. Given the specification of a protocol, we verify its properties by logical deduction. Reasoning techniques such as decomposition and abstraction are used to reduce the verification complexity. The transport protocol consists of an active process, a passive process, and two communication channels. Each of these components is specified by this model. An outline of verification of this protocol is given.

REFERENCES

• 1: K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
• 2: G.V. Bochmann, "Finite State Description of Communication Protocols," C.~om_~te~ Nej;works 2, 1978, 361-371.
• 3: G.V. Bochmann and C.A. Sunshine, "Formal Methods in Communication Protocol Design," I EE_~E Tr~D~actions on Commun!c~i_on_s COM- 28(4), April 1980, 624-631.
• 4: Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
• 5: C. H. Chow , M. G. Gouda , S. S. Lam, An exercise in constructing multi-phase communication protocols, Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium, p.42-49, June 06-08, 1984, Montréal, Quebec, Canada, United States
• 6: Mohamed G. Gouda , Khe-Sing The, Modeling physical layer protocols using communicating finite state machines, Proceedings of the ninth symposium on Data communications, p.54-62, September 1985, Whistler Moutain, British Columbia, Canada
• 7: B.T. Hailpern and S. Owicki, "Modular Verification of Computer Communication Protocol s,"IEEE Tr__~c_J;j_g~A 933 _C_o_m_~jj~_ca: +'.'or- 09~-~1~1~. ?~-'~'. *.':'.,~..':'-, "c~Cc'
• 8: James F. Kurose, The Specification and Verification of a Connection Establishment Protocol Using Temporal Logic, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.43-62, May 17-20, 1982
• 9: S.S. Lain and A.U. Shankar, "Protocol Verification via Projections,'riEE. E Transactions on Software Engineering SE-iO(7), July 1984, 325-342.
• 10: Richard L. Schwartz , P. M. Melliar-Smith, From State Machines to Temporal Logic: Specification Methods for Protocol Standards, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.3-19, May 17-20, 1982
• 11: N.V. Stenning, "A Data Transfer Protocol," g?m,p..y.~...er N e~ork }, ~er.+ember 1~w~, 99-~'0
• 12: C. Sunshine cl~: v. Dalai, "Connect ion Management in Transport Protocol s," Comauter Networks 2(6), December 1978, 4S4-473.
• 13: A.S. Tanenbaum, ~ J~LQ~, Prentice- Hal 1, Inc., 1981.
• 14: A.Y. Teng and M.T. L iu, "The Transamtssion Grammar Model for Protocol Construction," Trends and ADD1 tcatlons ~ Computer Ne.~.w.o.r~ Prg~.qc..o}.~., May 1980, ! 10-} ?0.
• 15: Raymond S. Tomlinson, Selecting sequence numbers, Proceedings of the 1975 ACM SIGCOMM/SIGOPS workshop on Interprocess communications, p.11-23, January 1975
• 16: O.H. West, "General Technique for Communications Protocol Validatlon," IBM ~~l of Research and Devel~j2lp_~d~t 22(4), July 1978, 393-404.
• 17: H. Z immermann, "0SI Reference Model -- The IS0 Model of Architecture for Open Systems Interconnectlon," IEEE IrAn~Actlgn~ on Co~)munic_at l on_s, CON-28(4), Ap r I 1 1980, 425- 432.

INDEX TERMS

Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
  C.2 COMPUTER-COMMUNICATION NETWORKS

General Terms:
Standardization, Verification