Formal verification of real-time software by symbolic model-checker

Verifications of real-time software are important. However, on the model-checking verifications, the state-explosion problem is serious. In this paper, we present a symbolic model-checking algorithm for real-time software, which can check CTL properties without computing exact states. Based on an approximation method, we formulate approximation/refinement procedure for symbolic model-checking, which recursively computes approximate states and iteratively refines approximations. The algorithm reduces the state-explosion using approximations of time zone and symbolic representations with DBMs(Difference Bounded Matrices) and BDDs(Binary Decision Diagrams). We have implemented the algorithm and experimented with CSMA/CD protocol. Experimental results show that our method can verify large real-time systems which cannot be handled by conventional symbolic model-checkers.