Path-based Model Checking
Wen Chien Liu and Chyan Goei Chung
National Chiao Tung University, Taiwan, ROC
Abstract
Model checking has been convinced to be an efficient and effective method of
formal verification of concurrent systems, and two types of underling
techniques are av ailable for model checking, i.e., state enumeration and
symbolic methods. However, they suffer from the state explosion problem or
the BDD node explosion problem. One key to break these problems is
to automatically separate the system into smaller subsystems that can be
verified independently so that the complexity of verification is reduced.
In our earlier paper, we have proposed a path-based approach to separate a
system into a set of concurrent path runs. Each run denotes a partial
execution behavior of the system. It can be generated and verified
independently. Thus, in this paper, we combine the path-based approach with
model checking to alleviate the explosion problems in model checking.
Keywords:
model checking, temporal logic, protocol verification, path-based approach, and
concurrent path