BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CSL-TR-80-192
       ENTRY:: December 01, 1994
ORGANIZATION:: Stanford University, Computer Systems Laboratory
       TITLE:: VERIFYING NETWORK PROTOCOLS USING TEMPORAL LOGIC
        TYPE:: Technical Report
      AUTHOR:: Hailpern, Brent T.
      AUTHOR:: Owicki, Susan S.
        DATE:: June 1980
       PAGES:: 21
    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.
       NOTES:: [Adminitrivia V1/Prg/19941201]
         END:: STAN//CSL-TR-80-192