Symbolic Approximations for Verifying Real-Time Systems.
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1994
- Accession Number
- ADA326032
Entities
People
- Howard Wong-toi
Organizations
- Stanford University