Report Number: CS-TR-95-1546
Institution: Stanford University, Department of Computer Science
Title: Symbolic Approximations for Verifying Real-Time Systems
Author: Wong-Toi, Howard
Date: December 1994
Abstract: Real-time systems are appearing in more and more applications
where their proper operation is critical, e.g. transport
controllers and medical equipment. However they are extremely
difficult to design correctly. One approach to this problem
is the use of formal description techniques and automatic
verification. Unfortunately automatic verification suffers
from the state-explosion problem even without considering
timing information. This thesis proposes a state-based
approximation scheme as a heuristic for efficient yet
accurate verification.
We first describe a generic iterative approximation algorithm
for checking safety properties of a transition system.
Successively more accurate approximations of the reachable
states are generated until the specification is provably
satisfied or not. The algorithm automatically decides where
the analysis needs to be more exact, and uses state
partitioning to force the approximations to converge towards
a solution. The method is complete for finite-state systems.
The algorithm is applied to systems with hard real-time
bounds. State approximations are performed over both timing
information and control information. We also approximate the
system's transition structure. Case studies include some
timing properties of the MAC sublayer of the Ethernet
protocol, the tick-tock service protocol, and a timing-based
communication protocol where the sender's and receiver's
clocks advance at variable rates.
http://i.stanford.edu/pub/cstr/reports/cs/tr/95/1546/CS-TR-95-1546.pdf