## 3 Materials and Methods
### Model Verification  
After constructing a system model in TLA+, it can be easily evaluated using TLC. In fact, TLC acts as a simulation tool that creates a graph in which the nodes represent the states and the edges represent the processes. This modeling and simulation method is more efficient than other simulation techniques, such as Monte Carlo simulation [26], because the entire state space can be evaluated in a short time and states that occur very rarely can also be examined. The results can be compared to the known best and worst-cases and an average and a standard deviation can also be calculated for the data quality. Before starting the model checker, we have to assign values to the defined constants. As is written in a former study [27], by increasing the number of variables in a system, the size of the system grows exponentially, which is called the \"state explosion problem\". However, the size of the state space can be limited by using or defining input variables with fixed values or intervals. Before starting the model checking and assigning an infinite set of numbers to the variables and huge values to the constants, we have made a prior calculation in order to estimate the complexity of the problem. Table 1 concludes the number of possible outcomes that would be verified using different values for total number of windows. The maximum number of windows defines when the model checker has to terminate. If we have 10 s long windows and the maximum number of windows is set to 1, we can only have \(2^{1-1}=1\) states, because the first window cannot be dropped because of latency. However, it is not true for the further states, so every other state can have two possible outcomes. All in all, it can be said that the number of possible states of the system can be calculated with the formula in Equation (5).  
\[2^{W-1}\,\ where\ W\in\mathbb{Z}^{+} \tag{5}\]If we were to evaluate a 24-h simulation within 1 s, it would take years to evaluate the entire state space. However, the problem is not as simple as it seems to be. The number of possible states would be much more if we tested the system with all possible latency values.  
We added three input variables, _UPLOAD_LATENCY_, _PROC_TIME_ALG_1_ and _PROC_TIME_ALG_2_. In order to limit the size of state space, we assign intervals to the input variables, so the model checker evaluates the model with all possible values from the intervals and we can still have a wide and focused state space that describes our system well. However, we still have to deal with the number of data windows because an ECG holder is usually worn for at least 24 h. On the one hand, the window size can be increased in order to have fewer data windows in a 24-h measurement, but the window size must be kept within reasonable limits to have interpretable data and not lose the real-time capability of the system. On the other hand, if we just simply terminate the simulation after a given number of evaluations, we cannot guarantee that our results are representative. In order to have accurate results for the data quality, we try to move the model parameters as close to reality as possible. If we use random values, we cannot be more accurate than a Monte Carlo simulation or a random test. All the three input variables can be approximated well if we know their behavior in the system. Based on their roles, we try to assign values from their distribution. If we assign values to the input variables from a distribution that describes the probability variable well, the simulations can also be informative after a small number of executions. Next, we present a methodology to find an accurate PDF based on real executions.