BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-90-1329
       ENTRY:: September 14, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: An interleaving model for real time.
        TYPE:: Technical Report
      AUTHOR:: Henzinger, Thomas A.
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: September 1990
       PAGES:: 37
    ABSTRACT:: The interleaving model is both adequate and sufficiently
               abstract to allow for the practical specification and
               verification of many properties of concurrent systems. We
               incorporate real time into this model by defining the
               abstract notion of a real-time transition system as a
               conservative extension of traditional transition systems:
               qualitative fairness requirements are replaced (and
               superseded) by quantitative lower-bound and upper-bound
               real-time requirements for transitions. We present proof
               rules to establish lower and upper real-time bounds for
               response properties of real-time transition systems. This
               proof system can be used to verify bounded-invariance and
               bounded-response properties, such as timely terrnination of
               shared-variables multi-process systems, whose semantics is
               defined in terms of real-time transition systems.
       NOTES:: [Adminitrivia V1/RAM/19940914]
         END:: STAN//CS-TR-90-1329