Tabled Resolution + Constraints: A Recipe for Model Checking Real-Time Systems

Xiaoqun Du, C. R. Ramakrishnan, Scott A. Smolka


We present a computational framework based on tabled resolution and constraint processing for verifying real-time systems. We also discuss the implementation of this framework in the context of the XMC/RT verification tool. For systems specified using timed automata, XMC offers backward and forward reachability analysis, as well as timed modal mu-calculus model checking. It can also handle timed infinite-state systems, such as those with unbounded message buffers, provided the set of reachable states is finite. We illustrate this capability on a real-time version of the leader election protocol. Finally, XMC/RT can function as a model checker for untimed systems. Despite this versatility, preliminary benchmarking experiments indicate that XMC/RT's performance remains competitive with that of other real-time verification tools.

Bibtex Entry:

author = {Xiaoqun Du and  C. R. Ramakrishnan and  Scott A. Smolka},
title = {Tabled Resolution + Constraints:  A Recipe for Model Checking Real-Time Systems},
booktitle = {IEEE Real Time Systems Symposium ({RTSS})},
address = {Orlando, Florida},
month = {November},
year = {2000}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan