@inproceedings{yang2009modist,
author = {Yang, Junfeng and Chen, Tisheng and Wu, Ming and Xu, Zhilei and Liu, Xuezheng and Lin, Haoxiang and Yang, Mao and Long, Fan and Zhang, Lintao and Zhou, Lidong},
title = {MODIST: Transparent Model Checking of Unmodified Distributed Systems},
booktitle = {NSDI 2009},
year = {2009},
month = {April},
abstract = {MODIST is the first model checker designed for transparently checking unmodified distributed systems running on unmodified operating systems. It achieves this transparency via a novel architecture: a thin interposition layer exposes all actions in a distributed system and a centralized, OS-independent model checking engine explores these actions systematically. We made MODIST practical through three techniques: an execution engine to simulate consistent, deterministic executions and failures; a virtual clock mechanism to avoid false positives and false negatives; and a state exploration framework to incorporate heuristics for efficient error detection.

We implemented MODIST on Windows and applied it to three well-tested distributed systems: Berkeley DB, a widely used open source database; MPS, a deployed Paxos implementation; and PACIFICA, a primary-backup replication protocol implementation. MODIST found 35 bugs in total. Most importantly, it found protocol-level bugs (i.e., flaws in the core distributed protocols) in every system checked: 10 in total, including 2 in Berkeley DB, 2 in MPS, and 6 in PACIFICA.},
publisher = {USENIX},
url = {http://approjects.co.za/?big=en-us/research/publication/modist-transparent-model-checking-of-unmodified-distributed-systems/},
pages = {213-228},
note = {The 6th Symposium on Networked Systems Design and Implementation},
}