Verification of Real-Time Systems by Successive
Over and Under Approximation
David L. Dill Howard Wong-Toi
Department of Computer Science Department of Computer Science
Stanford University Cornell University
dill@cs.stanford.edu howard@cs.cornell.edu
Automata-theoretic techniques provide a powerful means of verifying
finite-bounded systems. However they suffer from state explosion.
One approach to this problem is to analyze an abstracted system
description. In safety verification, different abstractions can yield
true lower or upper approximations of the set of reachable states.
Previously, we presented an algorithm~\cite{WD94} which uses simple
heuristics to automatically generate finer abstractions until the
approximations correctly answer the verification problem.
In this paper, we extend the algorithm to include approximations over
the system's transition structure as well as its state-space. In
terms of real-time system verification, this enables us to efficiently
verify properties of the full class of timed safety automata augmented
with urgency semantics. We describe a case study involving some
bounded liveness properties of the MAC sublayer of the Ethernet
protocol, based on a description by Weinberg and Zuck. This example
is substantially more difficult than those verified by previously
published real-time verification techniques.
Much of the algorithm's effectiveness is gained from the successful
combination of approximation techniques with a mixture of symbolic
representations for the state space. We use ordered binary decision
diagrams for control information and difference bounds matrices for
the timing information.