We introduce Fausta, an algorithmic traffic gener-ation platform that enables analysis and testing at scale. Fausta has been deployed at Meta to analyze and test the WhatsApp plat-form infrastructure since September 2020, enabling WhatsApp developers to deploy reliable code changes to a code base of millions of lines of code, supporting over 2 billion users who rely on WhatsApp for their daily communications. Fausta covers expected and unexpected program behaviors in a privacy-safe controlled environment to support multiple use cases such as reliability testing, privacy analysis and performance regression detection. It currently supports three different algorithmic input generation strategies, each of which construct realistic backend server traffic that closely simulates production data, without replaying any real user data. Fausta has been deployed and closely integrated into the WhatsApp continuous integration process, catching bugs in development before they hit production. We report on the development and deployment of Fausta's reliability use case between September 2020 and August 2021. During this period it has found 1,876 unique reliability issues, with a fix rate of 74%, indicating a high degree of true positive fault revelation. We also report on the distribution of fault types revealed by Fausta, and the correlation between coverage and faults found. Overall, we do find evidence that higher coverage is correlated with fault revelation.

Targeted property-based testing is an enhanced form of property-based testing (PBT) where the input generation is guided by a search strategy instead of being random, thereby combining the strengths of QuickCheck-like and search-based testing techniques. To use it, however, the user currently needs to specify a search strategy and also supply all ingredients that the search strategy requires. This is often a laborious process and makes targeted PBT less attractive than its random counterpart. In this paper, we focus on simulated annealing, the default search strategy of our tool, and present a technique that automatically creates all the ingredients that targeted PBT requires starting from only a random generator. Our experiments, comparing the automatically generated ingredients to fine-tuned manually written ones, show that the performance that one obtains is sufficient and quite competitive in practice.

We introduce targeted property-based testing, an enhanced form of property-based testing that aims to make the input generation component of a property-based testing tool guided by a search strategy rather than being completely random. Thus, this testing technique combines the advantages of both search-based and property-based testing. We demonstrate the technique with the framework we have built, called Target, and show its effectiveness on three case studies. The first of them demonstrates how Target can employ simulated annealing to generate sensor network topologies that form configurations with high energy consumption. The second case study shows how the generation of routing trees for a wireless network equipped with directional antennas can be guided to fulfill different energy metrics. The third case study employs Target to test the noninterference property of information-flow control abstract machine designs, and compares it with a sophisticated hand-written generator for programs of these abstract machines.

We advocate the use of property-based testing in the area of sensor networks and present a framework to apply this testing methodology. Our framework provides an expressive high-level language to specify a wide range of properties, starting from properties of individual functions to network-global properties, and infrastructure to automatically test these properties in Cooja, the network simulator of the Contiki operating system. We demonstrate the ease of use and effectiveness of our framework by two case studies. In the first, we test whether the energy consumption of the radio duty-cycle protocol X-MAC is within some specific bound. Property-based testing finds minimal network configurations where a small number of nodes violate the property. Property-based testing also reveals that the same property is not violated when ContikiMAC is used instead, but finds cases where ContikiMAC has higher energy consumption than X-MAC. In the second case study, we test the C API of CONTIKI's TCP socket library and find bugs in its event system that would be very hard to detect with other methods.