BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-94-1522
       ENTRY:: September 08, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Compositional Verification of Reactive and Real-time Systems
	TYPE:: Thesis
        TYPE:: Technical Report
      AUTHOR:: Chang, Edward
        DATE:: December 1993
       PAGES:: 115
    ABSTRACT:: This thesis presents a compositional methodology for the
               verification of reactive and real-time systems. The
               correctness of a given system is established from the
               correctness of the system's components, each of which may be
               treated as a system itself and further reduced. When no
               further reduction is possible or desirable, global techniques
               for verification may be used to verify the bottom-level
               components.

               Transition modules are introduced as a suitable compositional
               model of computation. Various composition operations are
               defined on transition modules, including parallel
               composition, sequential composition, and iteration. A
               restricted assumption-guarantee style of specification is
               advocated, wherein the environment assumption is stated as a
               restriction on the environment's next-state relation.
               Compositional proof rules are provided in accordance with the
               safety-progress hierarchy of temporal properties.

               The compositional framework is then extended naturally to
               real-time transition modules and discrete-time metric
               temporal logic.
       NOTES:: [Adminitrivia V1/Prg/19940908]
         END:: STAN//CS-TR-94-1522