BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CSL-TR-85-270
       ENTRY:: November 08, 1994
ORGANIZATION:: Stanford University, Computer Systems Laboratory
       TITLE:: A Model and Temporal Proof System for Networks of Processes
        TYPE:: Technical Report
      AUTHOR:: Nguyen, Van
      AUTHOR:: Gries, David
      AUTHOR:: Owicki, Susan
        DATE:: February 1985
       PAGES:: 12
    ABSTRACT:: A model and a sound and complete proof system for networks of
               processes in which component processes communicate
               exclusively through messages is given. The model, an
               extension of the trace model, can describe both synchronous
               and asynchronous networks. The proof system uses
               temporal-logic assertions on sequences of observations - a
               generalization of traces. The use of observations traces
               makes the proof system simple, compositional and modular,
               since internal details can be hidden. The expressive power of
               temporal logic makes it possible to prove temporal properties
               (safety, liveness, precedence, etc.) in the system. The proof
               system is language-independent and works for both synchronous
               and asynchronous networks.
       NOTES:: [Adminitrivia V1/Prg/19941108]
         END:: STAN//CSL-TR-85-270