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.