Department of Computer Science and Technology

Technical reports

Formal verification of real-time protocols using higher order logic

Rachel Cardell-Oliver

August 1990, 36 pages

DOI: 10.48456/tr-206

Abstract

A protocol is a distributed program which controls communication between machines in a computer network. Two or more programs are executed on different computers which communicate only via the medium connecting them.

Protocol implementations are difficult to understand and write correctly because the interaction between programs and their non-deterministic, real-time environment is complex. For this reason protocols are often specified using an abstract model. However few abstract specification techniques model the problems which occur in real implementations. In particular, the correctness of many protocols depends on real-time issues such as the correct setting of timers and fast responses to incoming messages.

This paper presents techniques for modelling real-time protocols at different levels of abstraction, from implementation behaviour to abstract requirements specifications. The language used for these models is higher order logic. The techniques are illustrated by the specification and verification of the class of sliding window protocols. The HOL system, a machine implementation of higher order logic [2], as used to both specify and verify this example and a full listing of the HOL theories for sliding window protocols is given in Appendix B.

Full text

PDF (1.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-206,
  author =	 {Cardell-Oliver, Rachel},
  title = 	 {{Formal verification of real-time protocols using higher
         	   order logic}},
  year = 	 1990,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-206.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-206},
  number = 	 {UCAM-CL-TR-206}
}