Formal Verification of the Binary Exponential Backoff Protocol

Jozef Hooman

Appeared in: Proc. Estonian Academy of Sciences (Special issue on the 9th Nordic Workshop on Programming Theory) Volume 4, Number 2, pages 89-105, 1998.


We present a formal framework for the specification and verification of distributed real-time systems. To obtain mechanical support, this framework has been defined in the language of the proof checker PVS. Intermediate stages of the design are represented by mixed terms where specifications and programming constructs can be combined. Compositional proof rules allow the verification of design steps. Here we focus on rules for parallel composition and hiding. Their use during protocol verification is illustrated by a part of the HTTP protocol, the binary exponential backoff protocol.