# SPOT: Testing Stream Processing Programs with Symbolic Execution and Stream Synthesizing
## 4 Time Series Stream Synthesis
### Modeling Stream  
To synthesize a time series of stream data, we need to generate timestamps and assign a timestamp to every timeless data that we have obtained in the symbolic execution phase. To describe the process in a formal way, we need to introduce some terminology.  
**Definition 1**.: _Stream data. Stream datum \(e\) is of a nested data type that mainly consists of the data value \(v\) and a timestamp \(t\), i.e., the stream datum is a tuple represented as \(e=(v,t)\)._  
In this definition, we regard one stream datum \(e\) as a compound datum composed of spatial and temporal data. Here, we refer to \(v\) as the spatial datum, as it represents how some specific JDU paths will be covered when running with this value. The temporal datum \(t\) is more straightforward, which is the physical time when the stream datum is generated (e.g., datum generated by remote sensors in IoT systems).  
**Definition 2**.: _Stream. A stream \(s\) is a sequence of stream data in a logical order: \(s=\langle e_{0},e_{1},...,\,e_{n}\rangle\), where the length of \(s\) can be finite or infinite._  
**Definition 3**.: _Logical order in stream data. We use \(\Leftarrow\) to represent the logical order of two stream data, which decides the order of these two data to be ingested by DSP programs._  
For instance, we write \(x\Leftarrow y\) to denote that during the test process, stream data \(y\) should be fed into the SUTs after stream data \(x\). This logical order is independent of the potential order basing on the timestamps in stream data. When conducting the test, we feed the SUT with the data from the time series stream one by one, following the logical order.  
**Definition 4**.: _Out-of-order stream data. We define two stream data \(x\) and \(y\) out-of-order as \(x\Leftarrow y\), but \(y.t<x.t\) where \(x.t\) and \(y.t\) represent timestamps of these two stream data individually._  
The logical order of two data will not always be compliant with order based on timestamps. Many metrics have been presented to measure the reordering, including reordering buffer occupancy density, reordering extent, and \(n\)-reordering, et cetera. [PERSON] et al. [42] have conducted a comparative analysis about these metrics.  
**Definition 5**.: _Orderness of a bounded stream. We define the orderness of a bounded stream \(s=\langle e_{0},e_{1},...,e_{n}\rangle\) following the similar notions of RD and entropy. We regard the stream in increasing order with regard to timestamp as the original order, and calculate entropy as the indicator to measure the degree of reordering for other out-of-order streams._  
For the bounded stream \(s=\langle e_{0},e_{1},...,e_{n}\rangle\), which follows a logical order \(e_{0}\Leftarrow e_{1}\Leftarrow...\Leftarrow e_{n}\), we can sort according to their timestamp from the earliest to the latest, getting the results \(s^{\prime}=\langle d_{0},d_{1},...,d_{n}\rangle\) where \(d_{0}.t\leqslant d_{1}.t\leqslant...d_{n}.t\) and \(\{e_{0},e_{1},...,e_{n}\}=\{d_{0},d_{1},...,d_{n}\}\). The sorted stream works as the baseline and indexed the data from \(0\) to \(n\). In our study, we assume that no duplicate data exist. For any datum, we can get its displacement by comparing its indices between \(s\) and \(s^{\prime}\). After getting the displacement of all stream data, we can then calculate the RD and further the entropy. In our study, we adopt entropy to guide our test process.  
For unbounded streams, we can split them based on a certain length of time (time window) or some number of data (count window) and measure the out-of-order degree for these stream fragments.  
Figure 5 shows two streams, each of which is composed of six stream data. Stream data on the right side are ingested before the ones on the left, and the right data are processed prior to the left data in logical order. The top of Figure 5 represents a reordering stream where the stream data B and D are late, and the bottom corresponds to its ordered version. We can calculate the entropy of the reordering stream to be \(1.56\).