In this report, we extend dynamic symbolic execution to distributed and concurrent systems. Dynamic symbolic execution can be used in software testing to systematically identify equivalence classes of input values and has been shown to scale well to large systems. Although usually restricted to sequential programs, this scalability makes it interesting to consider the technique in the distributed and concurrent setting as well. In order to extend the technique to concurrent systems, it is necessary to obtain sufficient control over the scheduling of concurrent activities to avoid race conditions. Creol, a modeling language for distributed concurrent objects, solves this problem by abstracting from a particular scheduling policy but explicitly defining scheduling points. This provides sufficient control to apply the technique of dynamic symbolic execution for model based testing of interleaved processes. The technique has been formalized in rewriting logic, executes in Maude, and applied to non-trivial examples, including an industrial case study.
This technical report contains the papers presented at Refine 2006, the International Refinement Workshop. This compendium is the preliminary proceedings for the workshop for the convenience of the workshop participants; the official proceedings will be published after the workshop in Electronic Notes on Theoretical Computer Science
