| This thesis proposes diagram-based formalisms to verify temporal properties of reactive systems. Reactive systems maintain an ongoing interaction with their environment and include discrete, real-time, and hybrid systems. Diagrams integrate deductive and algorithmic techniques for the verification of finite and infinite-state systems, thus combining the expressive power and flexibility of deduction with the automation provided by algorithmic methods.; Generalized verification diagrams represent the temporal structure of the program as relevant to the property they prove. The deductive component of a verification diagram defines a set of first-order verification conditions that, when proven valid, show that all behaviors of the system are embedded in the diagram. The algorithmic component is an automata-theoretic language inclusion check that determines whether all behaviors of the diagram satisfy the property.; Falsification diagrams represent behaviors of the system that do not satisfy the property. Deductive Model Checking incrementally refines these diagrams, removing behaviors that the system cannot exhibit, until no behaviors remain, which proves the property, or a counterexample is found.; We show how these methods can be used to verify not only discrete systems, but real-time and hybrid systems as well. We also present two specialized classes of diagrams for these systems: nonzenoness diagrams represent a proof that a real-time or hybrid system is time-divergent, that is, all behaviors of the system can be extended into behaviors in which time grows beyond any bound. Receptiveness diagrams prove a related property of real-time and hybrid modules that implies time divergence and is preserved by parallel composition. |
