Name
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. |
Year | Venue | Keywords |
|---|---|---|
2009 | NSDI | actions systematically,model checker,berkeley db,false positive,os-independent model checking engine,execution engine,primary-backup replication protocol implementation,paxos implementation,transparent model checking,false negative,unmodified operating system,model checking,distributed system,operating system,error detection |
Field | DocType | Citations |
Virtual clock,Transparency (graphic),Architecture,Model checking,Computer science,Real-time computing,Error detection and correction,Heuristics,False positives and false negatives,Operating system,Distributed computing,Paxos | Conference | 76 |
PageRank | References | Authors |
2.78 | 29 | 10 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Junfeng Yang | 1 | 1226 | 69.60 |
| Tisheng Chen | 2 | 76 | 2.78 |
| Ming Wu | 3 | 901 | 62.61 |
| Zhilei Xu | 4 | 187 | 10.42 |
| Xuezheng Liu | 5 | 352 | 22.72 |
| Haoxiang Lin | 6 | 181 | 9.29 |
| Mao Yang | 7 | 496 | 30.94 |
| Fan Long | 8 | 748 | 22.78 |
| Lintao Zhang | 9 | 3512 | 200.80 |
| Lidong Zhou | 10 | 2136 | 147.82 |