Faster FDR Counterexample Generation Using SAT-Solving

With the flourishing development of efficient SAT-solvers, bounded model checking (BMC) has proven to be an extremely powerful symbolic model checking technique.

In this talk, we address the problem of applying BMC to concurrent systems involving the interaction of multiple processes running in parallel. We demonstrate how the BMC framework can be adapted to the process-algebraic settings, and more specifically, to the context of CSP and FDR, resulting in a bounded refinement checking procedure. Refinement checking reduces to checking for reverse containment of behaviours. Therefore, we show how to exploit the SAT-solver to decide bounded language inclusion as opposed to bounded reachability of error states, as in most existing model checkers.

The focus in the talk is on the CSP traces semantic model, which is sufficient for verifying safety properties. We set out some necessary background information on CSP and FDR's hybrid two-level strategy for representing the operational semantics, which is also the basis for our Boolean encoding of CSP processes. Since the original syntactic translation of BMC to SAT cannot be applied directly to the context of CSP, we present a semantic translation algorithm based on watchdog transformations. We introduce a prototype tool, called SymFDR, and present a small number of experimental comparisons against FDR, FDR used in a non-standard way, a competing CSP model checker PAT, as well as, in some cases, NuSMV and Alloy Analyzer. Experiments indicate that sometimes SymFDR outperforms FDR significantly when finding counterexamples. This holds especially for complex combinatorial problems.

This is joint work with Bill Roscoe and Joel Ouaknine.