José Luis Conradi Hoffmann
ABSTRACT
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.
- Adina Aniculaesei, Andreas Vorwald, Meng Zhang, and Andreas Rausch. 2021. Architecture-based Hybrid Approach to Verify Safety-critical Automotive System Functions by Combining Data-driven and Formal Methods. In 2021 IEEE 18th International Conference on Software Architecture Companion (ICSA-C). 1–10. https://doi.org/10.1109/ICSA-C52384.2021.00036Google Scholar
Cross Ref
- Guangyao Chen and Zhihao Jiang. 2021. Environment Modeling During Model Checking of Cyberphysical Systems. Computer 54, 9 (2021), 49–58. https://doi.org/10.1109/MC.2021.3087631Google ScholarDigital Library
- Yue Cui, Pramod Bangalore, and Lina Bertling Tjernberg. 2021. A fault detection framework using recurrent neural networks for condition monitoring of wind turbines. Wind Energy 24, 11 (Feb. 2021), 1249–1262. https://doi.org/10.1002/we.2628Google ScholarCross Ref
- Ziquan Deng and Zhaodan Kong. 2021. Interpretable Fault Diagnosis for Cyberphysical Systems: A Learning Perspective. Computer 54, 9 (2021), 30–38. https://doi.org/10.1109/MC.2021.3078694Google ScholarDigital Library
- Antônio Augusto Fröhlich. 2018. SmartData: an IoT-ready API for sensor networks. International Journal of Sensor Networks 28, 3 (2018), 202.Google ScholarCross Ref
- José Luis Conradi Hoffmann and Antonio Augusto Frohlich. 2022. Embedding Anomaly Detection Autoencoders for Wind Turbines. In 2022 IEEE 27th International Conference on Emerging Technologies and Factory Automation (ETFA). IEEE. https://doi.org/10.1109/etfa52439.2022.9921541Google ScholarDigital Library
- José Luis Conradi Hoffmann and Antônio Augusto Fröhlich. 2022. SmartData Safety: Online Safety Models for Data-Driven Cyber-Physical Systems. In IECON 2022 – 48th Annual Conference of the IEEE Industrial Electronics Society. 1–6. https://doi.org/10.1109/IECON49645.2022.9969074Google ScholarCross Ref
- José Luis Conradi Hoffmann, Leonardo Passig Horstmann, Mateus Martínez Lucena, Gustavo Medeiros de Araujo, Antônio Augusto Fröhlich, and Marcos Hisashi Napoli Nishioka. 2021. Anomaly Detection on Wind Turbines Based on a Deep Learning Analysis of Vibration Signals. Applied Artificial Intelligence 35, 12 (Aug. 2021), 893–913. https://doi.org/10.1080/08839514.2021.1966879Google ScholarCross Ref
- Matthew Jablonski, Bo Yu, Gabriela Felicia Ciocarlie, and Paulo Costa. 2021. A Case Study in the Formal Modeling of Safe and Secure Manufacturing Automation. Computer 54, 9 (2021), 59–71. https://doi.org/10.1109/MC.2021.3087519Google ScholarDigital Library
- Yuchen Jiang, Shen Yin, and Okyay Kaynak. 2018. Data-Driven Monitoring and Safety Control of Industrial Cyber-Physical Systems: Basics and Beyond. IEEE Access 6 (2018), 47374–47384. https://doi.org/10.1109/ACCESS.2018.2866403Google ScholarCross Ref
- Jian-Qiang Lin, Ho-Chun Wu, and Shing-Chow Chan. 2021. A New Regularized Recursive Dynamic Factor Analysis With Variable Forgetting Factor and Subspace Dimension for Wireless Sensor Networks With Missing Data. IEEE Transactions on Instrumentation and Measurement 70 (2021), 1–13. https://doi.org/10.1109/TIM.2021.3083889Google ScholarCross Ref
- Jun Liu, Junnian Wang, Wenxin Yu, Zhenheng Wang, Guang’an Zhong, and Feng He. 2022. Semi-supervised deep learning recognition method for the new classes of faults in wind turbine system. Applied Intelligence (Jan. 2022). https://doi.org/10.1007/s10489-021-03024-8Google ScholarDigital Library
- Meiyi Ma, John A. Stankovic, and Lu Feng. 2021. Toward Formal Methods for Smart Cities. Computer 54, 9 (2021), 39–48. https://doi.org/10.1109/MC.2021.3082991Google ScholarDigital Library
- Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Yassine Lakhnech and Sergio Yovine (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 152–166.Google Scholar
- Dejan Nickovic and Tomoya Yamaguchi. 2020. RTAMT: Online Robustness Monitors from STL. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings(Lecture Notes in Computer Science, Vol. 12302), Dang Van Hung and Oleg Sokolsky (Eds.). Springer, 564–571. https://doi.org/10.1007/978-3-030-59152-6_34Google ScholarDigital Library
- Benjamin Noack, Marcus Baum, and Uwe D. Hanebeck. 2015. State estimation for ellipsoidally constrained dynamic systems with set-membership pseudo measurements. 2015 IEEE International Conference on Multisensor Fusion and Integration for Intelligent Systems (MFI) (2015), 297–302.Google ScholarCross Ref
- Roberto M. Scheffel and Antnio A. Frhlich. 2018. WSN Data Confidence Attribution Using Predictors. In 2018 Eighth Latin-American Symp. on Dependable Computing (LADC). IEEE. https://doi.org/10.1109/ladc.2018.00025Google ScholarCross Ref
- Roberto M Scheffel and Antônio A Fröhlich. 2019. Increasing sensor reliability through confidence attribution. Journal of the Brazilian Computer Soc. 25, 1 (2019), 1–20.Google ScholarCross Ref
- Roberto Milton Scheffel, José Luís Conradi Hoffmann, Leonardo Passig Horstma-nn, Gustavo Medeiros de Araujo, Antônio Augusto Fröhlich, Tiago Kaoru Matsuo, Vitor Pohlenz, and Marcos Hisashi Napoli Nishioka. 2020. Data Confidence Applied to Wind Turbine Power Curves. In 2020 X Brazilian Symposium on Computing Systems Engineering (SBESC). 1–8. https://doi.org/10.1109/SBESC51047.2020.9277861Google ScholarCross Ref
- S. A. Seshia, S. Hu, W. Li, and Q. Zhu. 2017. Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 36, 9 (2017), 1421–1434. https://doi.org/10.1109/TCAD.2016.2633961Google ScholarDigital Library
- S. Shalev-Shwartz, S. Shammah, and A. Shashua. 2017. On a formal model of safe and scalable self-driving cars. In arXiv preprint. arXiv:1708.06374v6Google Scholar
- Hao Ye, Le Liang, Geoffrey Ye Li, JoonBeom Kim, Lu Lu, and May Wu. 2018. Machine Learning for Vehicular Networks: Recent Advances and Application Examples. IEEE Vehicular Technology Magazine 13, 2 (2018), 94–101. https://doi.org/10.1109/MVT.2018.2811185Google ScholarCross Ref
- Junping Zhang, Fei-Yue Wang, Kunfeng Wang, Wei-Hua Lin, Xin Xu, and Cheng Chen. 2011. Data-Driven Intelligent Transportation Systems: A Survey. IEEE Transactions on Intelligent Transportation Systems 12, 4 (2011). https://doi.org/10.1109/TITS.2011.2158001Google ScholarDigital Library
Index Terms
- Using Formal Methods for On-The-Fly Time Series Verification
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Falsification of cyber-physical systems with robustness-guided black-box checking
HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and ControlFor exhaustive formal verification, industrial-scale cyber-physical systems (CPSs) are often too large and complex, and lightweight alternatives (e.g., monitoring and testing) have attracted the attention of both industrial practitioners and academic ...
Formal Verification of a Timing Enforcer Implementation
Special Issue ESWEEK 2017, CASES 2017, CODES + ISSS 2017 and EMSOFT 2017A timing enforcer is a scheduler that not only allocates CPU cycles to threads, but also uses timers to enforce time budgets. An approach for verifying safety properties of timing enforcers at the source code level is presented. We assume that the ...
Comments