A method of automatic proof for the specification and verification of protocols

ABSTRACT

In this paper we apply a method of automatic proof to verify some properties of a computer network protocol. The method used is defined as an extension of classical resolution to temporal operators (@@@@), (@@@@), (@@@@) and Until. We define a Precedes operator that is very useful for the specification of protocols. The method has the form of a set of recursive rules. The examples that we give are FIFO and LIFO queues and the alternating bit protocol, and the properties that we verify are livennes properties of the Sender and Receiver processes in order to prove a liveness property of the global system.

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: Bochmann G.V., "Logical Verification and implementation of protocols", Proc. Fourth Data Communications Symp. CACM/IEEE, 1975, 7.15-7.20.
• 3: Cavalli A.R., Farinas del Cerro L., "Resolution for Linear Temporal Logic", LITP, Université Paris VII, October 1982.
• 4: Ana R. Cavalli , Luis Fariñas del Cerro, A Decision Method for Linear Temporal Logic, Proceedings of the 7th International Conference on Automated Deduction, p.113-127, May 14-16, 1984
• 5: Ana R. Cavalli , Luis Fariñas del Cerro, Specification and Verification of Networks Protocols Using, Proceedings of the 6th Colloquium on International Symposium on Programming, p.59-73, April 17-19, 1984
• 6: Farinas del Cerro L., Lauth E., "Raisonnement temporel: une méthode de déduction", LSI, Université Paul Sabatier, Novembre 1982.
• 7: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 8: R. T. Hailpern, Verifying Concurrent Processes Using Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 9: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 10: Lamport L., "Specifiying Concurrent Programs Modules", Computer Science Laboratory, SRI International, June 1981.
• 11: Lamport L., "What good is temporal logic? ", Proceedings of Cong. IFIP 83, Paris, North Holland, 657-667.
• 12: Z Manna , Amir Pnueli, Verification of concurrent programs, Part I: The temporal framework, Stanford University, Stanford, CA, 1981
• 13: Z Manna , Amir Pnueli, Verification of concurrent programs: a temporal proof system, Stanford University, Stanford, CA, 1983
• 14: Manna Z., Wolper P., "Synthesis of Communication Processes from Temporal Logic Specifications", Department of Computer Science, Stanford University, Sept. 1981.
• 15: Melliar Smith M.P., Schwarts R.L., "Temporal Logic Specifications of distributed systems", Communication au Congrès Parallélisme et Systèmes distribués, Versailles, Avril 1981.
• 16: Melliar Smith M.P., Scwartz R., "From state machines to temporal logic specifications: specifications methods for protocols standards", IEEE Transactions on Communications, Vol. Com. 30, N° 12, December 1982.
• 17: Schwartz R., Melliar-Smith P.M., Vogt Friedich H., "An Interval Logic for higher level Temporal Reasoning", Report Computer Science Laboratory, SRI International, June 1983.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Verification

Keywords:
Automatic proofs, Liveness, Protocols, Queue, Resolution, Safety, Specifications, Temporal logic