Using Formal Methods for On-The-Fly Time Series Verification

In this work, we propose the utilization of Signal Temporal Logic (STL) for on-the-fly timing and plausibility analysis of time series produced in an Internet of Things environment and stored in a Cloud. Data plausibility comprises a wide range of solutions ranging from threshold verification of data to a more complex Machine Learning mechanism that learns to classify data. Nevertheless, these methods lack timing verification in order to corroborate sampling correctness in terms of time. We rely on SmartData constructs to express time series with sufficient metadata in regard to semantics, location, and timing. From these metadata we extract the necessary information in order to build property monitors using STL, allowing for automatic code generation free of human-introduced errors. The property monitors cover semantics and timing aspects of data belonging to a time series. Whenever data is inserted into the IoT platform, verification routines are triggered to build traces and analyze data. Finally, we demonstrate the usage of the proposed solution on a real IoT application.