SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions / Aug 2005
Workshop paper on temporal automata for protocol specifications at SPIN 2005. We presented SPLAT, a tool that makes model-checking more accessible by helping developers bridge the gap between complex applications and their abstract models. The key challenge we addressed was how non-experts could create accurate abstractions without inadvertently hiding critical bugs, and how to determine whether counter-examples represent genuine bugs or just modeling artifacts. SPLAT combines static model-checking with dynamic enforcement of abstractions to validate the correspondence between models and implementations.