Effective testing of distributed system
designs is challenging. This is because the
executions that lead to violations of
important safety or liveness properties
represent an infinitesimally small fragment of
the set of all possible behaviors the system
can exhibit. In this paper, we address this
challenge by proposing a technique that
automatically synthesizes a test
controller--- a program that guides the
search for buggy executions--- tailored to the
model of a distributed system-under-test (SUT)
and the property whose violation we are
interested in triggering. We focus our
solution on open systems in which the
test controller must govern both the
construction of messages injected into the SUT
by an external environment as well as the
order in which messages within the SUT are
sent and received. Our approach rests on two
technical innovations: first, we develop a
novel trace-based refinement type system
called Prophecy Automata Types that
describes both the history of the system and
its future behaviors using a symbolic variant
of linear temporal logic. Second, we use these
types to design a synthesis algorithm that
constructs a program in a DSL tailored for
expressing test controllers. Such programs
directly express faulty executions in the
target system by fixing the order in which
messages are communicated among actors, and
the contents of messages sent from an external
environment to trigger component actions. We
describe the implementation of our approach in
a tool, Clouseau, and present a comprehensive
evaluation on a set of diverse, non-trivial
benchmarks, including a case study of an
application model developed by a major cloud
vendor, to justify our technique.