Report Number: CSL-TR-80-192
Institution: Stanford University, Computer Systems Laboratory
Title: Verifying network protocols using temporal logic
Author: Hailpern, Brent T.
Author: Owicki, Susan S.
Date: June 1980
Abstract: Programs that implement computer communications protocols can
exhibit extremely complicated behavior, and neither informal
reasoning nor testing is reliable enough to establish their
correctness. In this paper we discuss the application of
program verification techniques to protocols. This approach
is more reliable than informal reasoning, but has the
advantage over formal reasoning based on finite-state models
that the complexity of the proof does not grow unmanageably
as the size of the program increases. Certain tools of
concurrent program verification that are especially useful
for protocols are presented: history variables that record
sequences of input and output values, temporal logic for
expressing properties that must hold in a future system state
(such as eventual receipt of a message), and module
specification and composition rules. The use of these
techniques is illustrated by verifying a simple data transfer
protocol from the literature.