Department of Computer Science and Technology

Technical reports

The specification and verification of sliding window protocols in higher order logic

Rachel Cardell-Oliver

October 1989, 25 pages

DOI: 10.48456/tr-183

Abstract

This report describes the formal specification and verification of a class of sliding window protocols using higher order logic. It is proved that a model for implementations of the protocol locically implies safety and liveness invariants, and that these invariants in turm imply an abstract specification of the protocol. The specification and implementation models used in the proof are based on techniques developed for hardware verification in HOL at Cambridge. This model and proof will eventually be used as the basis for a more general sliding window protocol model.

Full text

PDF (1.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-183,
  author =	 {Cardell-Oliver, Rachel},
  title = 	 {{The specification and verification of sliding window
         	   protocols in higher order logic}},
  year = 	 1989,
  month = 	 oct,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-183.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-183},
  number = 	 {UCAM-CL-TR-183}
}