Symbolic Approximations for Verifying Real-Time Systems

摘要

This thesis proposes a state-based approximation scheme as a heuristic forreducing the effort required in 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 it can be determined whether the specification is 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 algorithm is used to verify that systems with hard real-time bounds satisfy timed safety properties. 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.