Abstract:
Logic programming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabulation. But efficiency and practicality of such a model checker were not adequately addressed. In this paper we describe XMC/dbm, an efficient model checker for real-time systems using tabling. Performance gains in XMC/dbm directly arise from the use of a lightweight constraint solver combined with tabling. Specifically the timing constraints are represented by difference bound matrices which are encoded as Prolog terms. Operations on these matrices, the dominant component in real-time model checking, are shared using tabling. We provide experimental evidence that the performance of XMC/dbm is considerably better than our previous real-time model checker and is highly competitive to other well known real-time model checkers implemented in C/C++. An important aspect of XMC/dbm is that it can handle verification of systems consisting of untimed components with performance comparable to verification systems built specifically for untimed systems.
Bibtex Entry:
@inproceedings{PRR:ICLP02, author = {Giridhar Pemmasani and C. R. Ramakrishnan and I. V. Ramakrishnan}, title = {Efficient Model Checking of Real Time Systems Using Tabled Logic Programming and Constraints}, booktitle = {International Conference on Logic Programming ({ICLP})}, address = {Copenhagen, Denmark}, month = {July}, series = {Lecture Notes in Computer Science}, volume = {2401}, publisher = {Springer}, pages = {100--114}, year = {2002} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)