Report Number: CS-TR-98-1614
Institution: Stanford University, Department of Computer Science
Title: Decomposing, Transforming and Composing Diagrams: The Joys of
Modular Verification
Author: Alfaro, Luca de
Author: Manna, Z ohar
Author: Sipma, Henny
Date: October 1998
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/98/1614/CS-TR-98-1614.pdf