# SPOT: Testing Stream Processing Programs with Symbolic Execution and Stream Synthesizing
## 2 Overview
### Motivating Example  
Suppose that [PERSON] is a developer who will build several DSP programs to process millions of data 24/7 continuously from numerous sensors that have been deployed remotely. [PERSON] works as a tester who designs test suites to find any data that may lead to unexpected behaviors. The first program is to convert temperature values from English to metric units. [PERSON] implements the conversion process with one map operator, and the main part of this program is shown in Figure 0(a). The conversion is implemented in the map operator (line 2). In Flink, the _map_ operator is responsible for DataStream to DataStream transformation. Specifically, it takes one stream data as input and then produces another stream data as output. We can infer that this conversion is stateless and it will react to every stream data individually, regardless of whether it arrives early or late. Even though this program is reasonably plain, it represents a large class of DSP programs for which the order of input data will not impact the final results. The second program gives out a warning whenever any two consecutive temperature events occur beyond some certain threshold in a given interval, which is similar to the request in [29]. In Figure 0(b), [PERSON] first uses _keyBy_ operator to partition data streams according to their keys (line 2). In this program, the keys are the IDs of each sensor. Then, he adopts the _countWindow_ (i.e., count-based window) operator so that the computing is triggered whenever every two stream data with the same ID are ingested (line 3). He implements the data processing algorithms with the _apply_ operator (line 4). As we can infer, the results of this program will be impacted by the order of input source data. For instance, we have three streams denoted as \(S_{1}\), \(S_{2}\), and \(S_{3}\) (which can be infinite, but we only show four data for each stream) as shown in Figure 2, among which \(S_{1}\) is ingested by DSP systems in order, while the other two are not. We specify the threshold as 100 so that any stream data beyond 100 (which are represented as red circles) will potentially trigger the alarm. This program will emit an alarm after four data in \(S_{1}\) are processed, while there is no alarm for the other two. We also notice that the degree of out-of-order for \(S_{2}\) and \(S_{3}\) differs, but they share the same results (i.e., no alarms). The third program is to give out the highest temperature detected in a short period. In Figure 0(c), [PERSON] first uses the _keyBy_ operator to partition data streams according to their keys (line 2) similar to the program above. Then, he groups stream data into a time window (line 3). He calculates the highest temperature by applying _max_ to the stream data in each time window. The order of stream data will impact the results. For example, if the highest temperature value arrives late after the window it belongs to, then an incorrect result may occur. The results will not be influenced when the low-temperature values are out of order, or the highest temperature is late but still in the required time window. We can draw several conclusions from the above three programs. (1) Reordering stream data may damage the correctness of DSP programs. (2) The degree of reordering may lead to different effects. In other words, some DSP programs may be tolerant of some kind of out-of-order, while some other programs will produce incorrect results as soon as a bit disorder happens. [PERSON], the tester, can easily design the test data if path coverage is the only target. For programs (a) and (c), any non-null test data will achieve 100% path coverage. For program (b), she can reach the same path coverage goal when the _apply_ operator does not contain any branches inside. However, when taking input data reordering into consideration, she has to build multiple test data first and then composes them into streams with some temporal orders to simulate different degrees of out-of-order.