Synthesizing Test Controllers from Types: Property-Guided Bug-Finding for Distributed System Models

Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan

abstract

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.