Abstract:
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:
@inproceedings{DRS:RTSS00, 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] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)