Report Number: CS-TR-94-1522
Institution: Stanford University, Department of Computer Science
Title: Compositional Verification of Reactive and Real-time Systems
Author: Chang, Edward
Date: December 1993
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/94/1522/CS-TR-94-1522.pdf