Model checking distributed systems by combining caching and process checkpointing
Abstract
Verification of distributed software systems by model checking is not a straightforward task due to inter-process communication. Many software model checkers only explore the state space of a single multi-threaded process. Recent work proposes a technique that applies a cache to capture communication between the main process and its peers, and allows the model checker to complete state-space exploration. Although previous work handles non-deterministic output in the main process, any peer program is required to produce deterministic output. This paper introduces a process checkpointing tool. The combination of caching and process checkpointing makes it possible to handle non-determinism on both sides of communication. Peer states are saved as checkpoints and restored when the model checker backtracks and produces a request not available in the cache. We also introduce the concept of strategies to control the creation of checkpoints and the overhead caused by the checkpointing tool.
BibTeX
@inproceedings{Leungwattanakit-al:ASE11,
author = {Watcharin Leungwattanakit and
Cyrille Artho and
Masami Hagiya and
Yoshinori Tanabe and
Mitsuharu Yamamoto},
title = {Model checking distributed systems by combining caching and process checkpointing},
booktitle = {ASE},
pages = {103--112},
publisher = {{IEEE} Computer Society},
year = {2011},
}