Affiliations: Graduate Student Department of Computer Science Stanford University
Research Interests: Formal Methods, Verification, Hybrid Systems, Reliability, Software Engineering, Temporal Logics
We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems (CPTSs), the specification language of Hybrid Temporal Logic (HTL), the graphical system description language of Hybrid Automata, and a proof system for verifying that hybrid automata satisfy their HTL specifications. The novelty of the approach lies in the continuous-time logic, which allows specification of both point-based and interval-based properties (ie. properties which describe changes over an interval) and provides direct references to derivatives of variables, and in the proof system that supports verification of point-based and interval-based properties. The proof rules demonstrate that sound and convenient induction rules can be established for continuous-time logics. The proof rules are illustrated on several examples.
We present a methodology for the verification of temporal properties of hybrid systems. The methodology is based on the deductive transformation of hybrid diagrams, which represent the system and its properties, and which can be algorithmically checked against the specification. This check either gives a positive answer to the verification problem, or provides guidance for the further transformation of the diagrams. The resulting methodology is complete for quantifier-free linear-time temporal logic.
The Computer Science Department home page.
The Theory Division home page.