We present a hybrid model checking algorithm for incomplete timed systems where parts of the system are unspecified (so-called black boxes). Here, we answer the question of unrealisability, i.e., "Is there a path violating a safety property regardless of the implementation of the black boxes?" Existing bounded model checking (BMC) approaches for incomplete timed systems exploit the power of modern SMT solvers, but might be too coarse as an abstraction for certain problem instances. On the other hand, symbolic model checking (SMC) for incomplete timed systems is more accurate, but may fail due to the size of the explored state space. In this work, we propose a tight integration of a backward SMC routine with a forward BMC procedure leveraging the strengths of both worlds. The symbolic model checker is hereby used to compute an enlarged target which we then try to hit using BMC. We use learning strategies to guide the SMT solver's search into the right direction and manipulate the enlarged target to improve the overall accuracy of the current verification run. Our experimental results show that the hybrid approach is able to verify incomplete timed systems which are out of the scope for BMC and can neither be solved in reasonable time using SMC. Furthermore, our approach compares favourably with UPPAAL-TIGA when considering timed games as a special case of the unrealisability problem.
展开▼
