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.
ABSTRACT
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.
Postscript