BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-98-1614
       ENTRY:: October 16, 1998
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Decomposing, Transforming and Composing Diagrams: The Joys of
               Modular Verification
        TYPE:: Technical Report
      AUTHOR:: Alfaro, Luca de
      AUTHOR:: Manna, Zohar
      AUTHOR:: Sipma, Henny
        DATE:: October 1998
       PAGES:: 13
    ABSTRACT:: The paper proposes a modular framework for the verification
               of temporal logic properties of systems based on the
               deductive transformation and composition of diagrams. The
               diagrams represent abstractions of the modules composing the
               system, together with information about the environment of
               the modules. The proof of a temporal specification is
               constructed with the help of diagram transformation and
               composition rules, which enable the gradual decomposition of
               the system into manageable modules, the study of the modules,
               and the final combination of the diagrams into a proof of the
               specification. We illustrate our methodology with the modular
               verification of a database demarcation protocol.
       NOTES:: [Adminitrivia V1/Prg/19981016]
         END:: STAN//CS-TR-98-1614