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.
Keywords for this software
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Morse, Everett; Vrvilo, Nick; Mercer, Eric; McCarthy, Jay: Modeling asynchronous message passing for C programs (2012)