An Optimizing Compiler for Efficient Model Checking

Abstract:

Different model checking tools offer a variety of specification languages to encode systems. These specifications are compiled into an intermediate form from which the global automata are derived at verification time. Some tools, such as SPIN, provide the user with constructs that can be used to affect the size of the global automata. In other tools, such as Murphi, the user specifies a system directly in terms of its global automata using a guarded command language, and hence has complete control over the automata sizes. Our experience shows that using low-level specifications we can significantly reduce verification times. The question then is, whether we can derive the low-level representations directly from a high-level specification without user intervention or dependence on user annotations.

We address this problem in this paper. We develop an optimizing compilation technique that transforms high-level specifications based on value-passing CCS into rules from which transitions of the global automata can be efficiently generated. The representation of rules is such that possible synchronizations can be computed at compile time in polynomial time while transitions can be generated during verification in unit time modulo indexing. We show, via experiments using examples with different characteristics, that our technique is very effective in practice. For example, the compiler reduces the verification time of our XMC model checker by a factor of up to fifteen, while reducing the space requirements by up to an order of magnitude. More importantly, we identify a set of optimizations that can be implemented with little compile-time overhead and significantly reduce the time and space required for verification.

Bibtex Entry:

@inproceedings{DR:FORTE99,
author = {Yifei Dong and  C. R. Ramakrishnan},
title = {An Optimizing Compiler for Efficient Model Checking},
booktitle = {Formal Methods for Protocol Engineering and Distributed Systems ({FORTE})},
address = {Beijing, China},
month = {October},
publisher = {Kluwer},
series = {IFIP Conference Proceedings},
volume = {156},
pages = {241--256},
year = {1999}
}

Full Paper:

[pdf]

C. R. Ramakrishnan
(cram@cs.sunysb.edu)