Report Number: CS-TR-97-1594
Institution: Stanford University, Department of Computer Science
Title: Interval and Point-Based Approaches to Hybrid System
Verification
Author: Kapur, Arjun
Date: September 1997
Abstract: Hybrid systems are real-time systems consisting of both
continuous and discrete components. This thesis presents
deductive and diagrammatic methodologies for proving
point-based and interval-based properties of hybrid systems,
where the hybrid system is modeled in either a sampling
semantics or a continuous semantics. Under a sampling
semantics the behavior of the system consists of a discrete
number of system snapshots, where each snapshot records the
state of the system at a particular moment in time. Under a
continuous semantics, the system behavior is given by a
function mapping each point in time to a system state. Two
continuous semantics are studied: a continuous interval
semantics, where at any given point in time the system is in
a unique state, and a super-dense semantics, where no such
requirement is needed.
We use Linear-time Temporal Logic for expressing properties
under either a sampling semantics or a super-dense semantics,
and we introduce Hybrid Temporal Logic for expressing
properties under a continuous interval semantics. Linear-time
Temporal Logic is useful for expressing point-based
properties, whose validity is dependent on individual states,
while Hybrid Temporal Logic is useful for expressing both
interval-based properties, whose validity is dependent on
intervals of time, and point-based properties.
Finally, two different verification methodologies are
presented: a diagrammatic approach for verifying properties
specified in Linear-time Temporal Logic, and a deductive
approach for verifying properties specified in Hybrid
Temporal Logic.
http://i.stanford.edu/pub/cstr/reports/cs/tr/97/1594/CS-TR-97-1594.pdf