Runtime verification in uncertain environment based on probabilistic model learning

Ge Zhou; Chunzheng Yang; Peng Lu; Xi Chen; Ge Zhou; Chunzheng Yang; Peng Lu; Xi Chen

doi:10.3934/mbe.2022635

Mathematical Biosciences and Engineering

2022, Volume 19, Issue 12: 13607-13627. doi: 10.3934/mbe.2022635

Previous Article Next Article

Research article Special Issues

Runtime verification in uncertain environment based on probabilistic model learning

1.
Department of Computer Science and Technology, National University of Defense Technology, Hunan, Changsha 410081, China
2.
Moral Culture Research Center, Hunan Normal University, Hunan, Changsha 410073, China
3.
School of Economics and Management, Xinjiang University, Xinjiang, Urumqi 830049, China
4.
Staff Department of Hunan Armed Police Corps, Hunan, Changsha 410022, China

Academic Editor: Runzhang Xu

Received: 21 June 2022 Revised: 11 August 2022 Accepted: 15 August 2022 Published: 16 September 2022

Runtime verification (RV) is a lightweight approach to detecting temporal errors of system at runtime. It confines the verification on observed trajectory which avoids state explosion problem. To predict the future violation, some work proposed the predictive RV which uses the information from models or static analysis. But for software whose models and codes cannot be obtained, or systems running under uncertain environment, these predictive methods cannot take effect. Meanwhile, RV in general takes multi-valued logic as the specification languages, for example the $ true $, $ false $ and $ inconclusive $ in three-valued semantics. They cannot give accurate quantitative description of correctness when $ inconclusive $ is encountered. We in this paper present a RV method which learns probabilistic model of system and environment from history traces and then generates probabilistic runtime monitor to quantitatively predict the satisfaction of temporal property at each runtime state. In this approach, Hidden Markov Model (HMM) is firstly learned and then transformed to Discrete Time Markov Chain (DTMC). To construct incremental monitor, the monitored LTL property is translated into Deterministic Rabin Automaton (DRA). The final probabilistic monitor is obtained by generating the product of DTMC and DRA, and computing the probabilities for each state. With such a method, one can give early warning once the probability of correctness is lower than a pre-defined threshold, and have the chance to do adjustment in advance. The method has been implemented and experimented on real UAS (Unmanned Aerial Vehicle) simulation platform.
- runtime verification,
- probabilistic monitor,
- Markov Chain,
- $ \omega $-automata
Citation: Ge Zhou, Chunzheng Yang, Peng Lu, Xi Chen. Runtime verification in uncertain environment based on probabilistic model learning[J]. Mathematical Biosciences and Engineering, 2022, 19(12): 13607-13627. doi: 10.3934/mbe.2022635

Related Papers:

Abstract

Runtime verification (RV) is a lightweight approach to detecting temporal errors of system at runtime. It confines the verification on observed trajectory which avoids state explosion problem. To predict the future violation, some work proposed the predictive RV which uses the information from models or static analysis. But for software whose models and codes cannot be obtained, or systems running under uncertain environment, these predictive methods cannot take effect. Meanwhile, RV in general takes multi-valued logic as the specification languages, for example the $ true $, $ false $ and $ inconclusive $ in three-valued semantics. They cannot give accurate quantitative description of correctness when $ inconclusive $ is encountered. We in this paper present a RV method which learns probabilistic model of system and environment from history traces and then generates probabilistic runtime monitor to quantitatively predict the satisfaction of temporal property at each runtime state. In this approach, Hidden Markov Model (HMM) is firstly learned and then transformed to Discrete Time Markov Chain (DTMC). To construct incremental monitor, the monitored LTL property is translated into Deterministic Rabin Automaton (DRA). The final probabilistic monitor is obtained by generating the product of DTMC and DRA, and computing the probabilities for each state. With such a method, one can give early warning once the probability of correctness is lower than a pre-defined threshold, and have the chance to do adjustment in advance. The method has been implemented and experimented on real UAS (Unmanned Aerial Vehicle) simulation platform.

References

[1]	P. Zhang, Z. Su, Y. Zhu, W. Li, B. Li, Ws-psc monitor: A tool chain for monitoring temporal and timing properties in composite service based on property sequence chart, in International Conference on Runtime Verification, 6418 (2010), 485–489. https://doi.org/10.1007/978-3-642-16612-9_39
[2]	I. O. Electrical, I. S. Board, IEEE standard for software verification and validation, Software Qual. Prof., 2005 (2005), 1–217. https://doi.org/10.1109/IEEESTD.2005.96278 doi: 10.1109/IEEESTD.2005.96278
[3]	E. M. Clarke, Model checking-my 27-year quest to overcome the state explosion problem, in 2009 24th Annual IEEE Symposium on Logic In Computer Science, IEEE, (2008). https://doi.org/10.1109/LICS.2009.42
[4]	O. J. Dahl, E. W. Dijkstra, C. A. R. Hoare, Structured Programming, Academic Press, 1972. https://doi.org/10.5555/1243380
[5]	C. Zhao, W. Dong, J. Wang, P. Sui, Z. Qi, Software active online monitoring under anticipatory semantics, Shm, 2009. Available from: https://smcit.ecs.baylor.edu/2011/www-smcit09/abstracts-contri_papers/karsai/DongWei_SHM.pdf.
[6]	K. Yu, Z. Chen, W. Dong, A predictive runtime verification framework for cyber-physical systems, in 2014 IEEE Eighth International Conference on Software Security and Reliability-Companion, (2014), 247–250. https://doi.org/10.1109/SERE-C.2014.43
[7]	A. Bauer, M. Leucker, C. Schallhart, Comparing ltl semantics for runtime verification, J. Log. Comput., 20 (2010), 651–674. https://doi.org/10.1093/logcom/exn075 doi: 10.1093/logcom/exn075
[8]	A. Naskos, E. Stachtiari, P. Katsaros, A. Gounaris, Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources, Springer International Publishing, 9333 (2015). https://doi.org/10.1007/978-3-319-23820-3_18
[9]	A. Filieri, G. Tamburrelli, Probabilistic verification at runtime for self-adaptive systems, in Assurances for Self-Adaptive Systems, 7740 (2013). https://doi.org/10.1007/978-3-642-36249-1_2
[10]	A. Nouri, B. Raman, M. Bozga, A. Legay, S. Bensalem, Faster statistical model checking by means of abstraction and learning, in Runtime Verification, 8734 (2014), 340–355. https://doi.org/10.1007/978-3-319-11164-3_28
[11]	U. Sammapun, I. Lee, O. Sokolsky, J. Regehr, Statistical runtime checking of probabilistic properties, Springer, Berlin Heidelberg, 2007 (2007). https://doi.org/10.1007/978-3-540-77395-5_14
[12]	V. C. Ngo, A. Legay, V. Joloboff, Pscv: A runtime verification tool for probabilistic systemc models, in International Conference on Computer Aided Verification, 9779 (2016). https://doi.org/10.1007/978-3-319-41528-4_5
[13]	J. Jayaputera, I. Poernomo, H. Schmidt, Runtime verification of timing and probabilistic properties using wmi and.net, in Proceedings. 30th Euromicro Conference, IEEE, (2004), 100–106. https://doi.org/10.1109/EURMIC.2004.1333361
[14]	C. Zhao, W. Dong, Z. Qi, Active monitoring for control systems under anticipatory semantics, in 2010 10th International Conference on Quality Software, (2010), 318–325. https://doi.org/10.1109/QSIC.2010.82
[15]	H. He, Z. Zou, "Black-box modeling of ship maneuvering motion using system identification method based on bp neural network, " in The 39th International Conference on Ocean, Offshore and Arctic Engineering, (2020). https://doi.org/10.1115/OMAE2020-18069
[16]	S. Kundu, A. Soyyigit, K. A. Hoque, K. Basu, "High-level modeling of manufacturing faults in deep neural network accelerators, " in 2020 IEEE 26th International Symposium on On-Line Testing and Robust System Design (IOLTS), (2020). https://doi.org/10.1109/iolts50870.2020.9159704
[17]	D. Angluin, Learning regular sets from queries and counterexamples, Inf. Comput., 75 (1987), 87–106. https://doi.org/10.1016/0890-5401(87)90052-6 doi: 10.1016/0890-5401(87)90052-6
[18]	Y. Kan, K. Yue, H. Wu, X. Fu, Z. Sun, Online learning of parameters for modeling user preference based on bayesian network, Int. J. Uncertainty Fuzzines Knowledge Based Syst., 30 (2022), 285–310. https://doi.org/10.1142/S021848852250012X \newpage doi: 10.1142/S021848852250012X
[19]	S. Tao, J. Jiang, D. Lian, K. Zheng, E. Chen, Predicting human mobility with reinforcement-learning-based long-term periodicity modeling, ACM Tran. Intell. Syst. Technol., 12 (2021), 1–23. https://doi.org/10.1145/3469860 doi: 10.1145/3469860
[20]	V. Forejt, M. Kwiatkowska, D. Parker, H. Qu, M. Ujma, Incremental runtime verification of probabilistic systems, in International Conference on Runtime Verification, 7687 (2012), 314–319. https://doi.org/10.1007/978-3-642-35632-2_30
[21]	A. Ferrando, G. Delzanno, Incrementally predictive runtime verification. in CILC, (2021), 92–106. https://doi.org/10.1007/978-3-642-28891-3_37
[22]	S. D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S. A. Smolka, et al., Runtime verification with state estimation, in International Conference on Runtime Verification, (2011), 193–207. https://doi.org/10.1007/978-3-642-29860-8_15
[23]	E. Bartocci, R. Grosu, A. Karmarkar, S. A. Smolka, S. D. Stoller, E. Zadok, et al., Adaptive runtime verification, in International Conference on Runtime Verification. (2012), 168–182. https://doi.org/10.1007/978-3-642-35632-2_18
[24]	Z. Chen, O. Wei, Z. Huang, H. Xi, Formal semantics of runtime monitoring, verification, enforcement and control, in International Symposium on Theoretical Aspects of Software Engineering, (2015), 63–70. https://doi.org/10.1109/TASE.2015.11
[25]	D. Giannakopoulou, K. Havelund, Runtime analysis of linear temporal logic specifications, in IEEE International Conference on Automated Software Engineering, (2001). Available from: http://www.riacs.edu/trs/.
[26]	S. M. Chu, T. S. Huang, An experimental study of coupled hidden markov models, in IEEE International Conference on Acoustics, Speech, and Signal Processing, (2002). https://doi.org/10.1109/ICASSP.2002.5745559
[27]	N. M. Abbasi, Hidden markov methods. algorithms and implementation, 2015. Available from: https://manualzz.com/doc/o/cklvd/.
[28]	B. Motik, Y. Nenov, R. Piro, I. Horrocks, Incremental update of datalog materialisation: the backward/forward algorithm, in Twenty-Ninth AAAI Conference on Artificial Intelligence, (2015), 1560–1568. https://doi.org/10.5555/2886521.2886537
[29]	An simulation platform of unmanned aerial vehicle. Available from: https://www.ardupilot.org/.
[30]	S. Safra, On the complexity of $\omega$-automata, in Foundations of Computer Science, W. H. Freeman, (1988), 319–327. https://doi.org/10.1109/SFCS.1988.21948
[31]	P. Gastin, D. Oddoux, Fast LTL to Büchi automata translation, in International Conference on Computer Aided Verification, (2001), 53–65. https://doi.org/10.1007/3-540-44585-4_6
[32]	LTL to deterministic Streett and Rabin automata. Available from: https://www.ltl2dstar.de/.
[33]	W. Liu, F. Song, G. Zhou, Reasoning about periodicity on infinite words, Appl. Microbiol. Biotechnol., 2017 (2017), 200–215. https://doi.org/10.1007/978-3-319-69483-2_12 doi: 10.1007/978-3-319-69483-2_12

Reader Comments

Your name:*

Email:*
© 2022 the Author(s), licensee AIMS Press. This is an open access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0)