Symbolic approximations for verifying real-time systems
Howard Wong-Toi · 1995
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 must consider the sequencing and coordination of events in different processes, as well as the times they occur. One approach to this problem is the use of formal description techniques and automatic verification. Unfortunately automatic verification suffers from the state-real-time explosion problem and is computationally expensive even without real-time. The addition of timing information makes the problem much harder. This thesis proposes a state-based approximation scheme as a heuristic for reducing the effort required in verification. We first describe a generic iterative approximation algorithm for checking safety properties of a transition system. It is designed to exploit the fact that not all the details of a system need to be considered in order to prove it correct. 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. In the case of finite-state systems, the method is complete. 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 describe some examples of successful verification, and successful error-detection. Case studies include some timing properties of the MAC sublayer of the Ethernet protocol, and a timing-based communication protocol where the sender's and receiver's clocks advance at variable rates.