## 3 Materials and Methods
### System Specification  
We find it important to verify systems not only before release, but also in the period of design to see if the concept may work or not. Standalone algorithms can be implemented and tested before a system is built, but no one can see what states a system would end up in if the components worked together. System models can be used to design a system and validate if they are conceptually and algorithmically correct. TLA+ is a tool for specifying systems and algorithms and creating a logical description. TLA+ Model Checker, called TLC, is responsible for verifying the correctness of the model. We elaborated a system model related to the selected use case in order to validate how data quality may vary under specific conditions. Our goal is to measure the data quality of the AF detection system, so we defined four checkpoints over the entire data path. 1. Raw ECG data collection in pre-defined window size. 2. Raw ECG data uploaded to the cloud. 3. Result of the AF detection algorithm is available in the cloud. 4. Result of the AF classification algorithm is available in the cloud. Figure 4 presents the model in graphic form. \(W_{i}\) denotes the \(i\)th window size in time, \(U_{i}\) stands for the time needed for uploading the raw ECG data of the \(i\)th window, \(T_{i}\) is the timeout value of the \(i\)th started request, and \(P_{ji}\) is the execution time of the \(i\)th algorithm having the data as an input of the \(j\)th window. As depicted in Figure 4, the window size is a constant value in the model. It has to be guaranteed that the sum of the ith upload time and the ith timeout value must be less than the window size. If the data is continuously uploaded to the cloud, the first algorithm  
Figure 4: Visualization of the system components on the axis of time. must produce a result before the timeout of the next data upload. If the latency of the first algorithm in the ith window is greater than the sum of the \(i+1\)th window size, the \(i+1\)th upload time and the \(i+1\)th timeout value, then \(W_{i+1}\) is dropped and only the \(W_{i+2}\) window can be processed. Furthermore, the condition for the \(j\)th algorithm (where \(j\
eq 1\)) is that it must finish before processing in the next window is finished by the algorithm preceding it. The latter conditions depend on the former ones. If the conditions defined in Equations (1)-(4) meet, no data loss can be present due to latency. \[U_{i}+T_{i}\leq W_{i}\;,\;\textit{where}\;i\in\mathbb{Z}^{+} \tag{1}\]  
\[P_{1i\_start}\leq T_{i\_end}\;,\;\textit{where}\;i\in\mathbb{Z}^{+} \tag{2}\]  
\[P_{1i}\leq W_{i+1}+U_{i+1}+T_{i+1}\;,\;\textit{where}\;i\in\mathbb{Z}^{+} \tag{3}\]  
\[P_{ji\_end}\leq P_{ji+1_{\textit{out}}}\;,\;\textit{where}\;i,j\in\mathbb{Z}^{+} \;\textit{and}\;j>1 \tag{4}\]  
Figure 5 presents the transformation applied on the data and functions that affect the results. \(d(\textit{raw})\) represents the raw ECG data obtained from the IoT sensor. After a defined time, the collected raw data form a data window. Here we can measure data quality if needed but in our offline case the data is available. The data window is sent to the AF detection algorithm that produces the output as to whether AF is detected and how long the episode is. Here, a data quality measurement can be performed because some windows may be lost. The \(d(af)\) results can be forwarded to the classification algorithm, where a new data quality measurement can be performed after a possible deterioration in the quality of the input data. A dropped data window can significantly degrade data quality but may have more severe consequences following an additional aggregation step. This is crucial in real-time systems, especially when it affects human lives. Based on this phenomenon, we consider it important to analyze how such a system works and how data quality changes when some of the data parts are lost. Using the conditions presented in Equations (1)-(4), we have implemented the model in TLA+. The formal definition of the system can be seen here.