Runtime Verification of States Unobservable Cyber-Physical System
FANG Bing-wu1,2, HUANG Zhi-qiu1, WANG Yong1, LI Yong1
1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu 210016, China;
2. School of YunGui Information, Anhui Finance and Trade Vocational College, Hefei, Anhui 230601, China
Abstract：Ensuring the correct behavior of cyber physical systems (CPS) at runtime is critical,and it is more so in safety-critical area,such as aerospace,automotive,nuclear power and medical.A method of runtime safety verification based on hidden Markov model (HMM) is proposed for the CPS with stochastic behavior and unobservable states.First,a runtime safety verification framework of the CPS is constructed where the system model is represented by HMM,and the negation of safety property is specified by deterministic finite automaton (DFA),and then the product automata of DFA and HMM is used as a runtime monitor.Thus,the problem of CPS runtime safety verification is reduced into a probabilistic inference problem on the monitor.Second,an incremental iterative safety verification algorithm and a counterexample generation algorithm are proposed.The experimental results show that the prediction error rate of the safety verification algorithm is nearly 20% lower than that of the particle filter algorithm.When the system violates the safety property,the proposed method can product a counterexample which the particle filtering method cannot do.
[1] 黄志球,徐丙凤,阚双龙,胡军,陈哲.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报,2014,25(2):200-218. Huang ZQ,Xu BF,Kan SL,Hu J,Chen Z.Survey on embedded software safety analysis standards,methods and tools for airborne system[J].Journal of Software,2014,25(2):200-218.(in Chinese)
[2] Chen F,Ye H,Yang J,et al.A standardized design methodology for complex digital logic components of cyber-physical systems[J].Microprocessors & Microsystems,2015,39(8):1245-1254.
[3] Zheng X,Julien C,Chen H,et al.Real-time simulation support for runtime verification of cyber-physical systems[J].ACM Transactions on Embedded Computing Systems,2017,16(4):106.
[4] Jiang Y,Song H,Wang R,et al.Data-centered runtime verification of wireless medical cyber-physical system[J].IEEE Transactions on Industrial Informatics,2017,13(4):1900-1909.
[5] Medhat R,Bonakdarpour B,Kumar D,et al.Runtime monitoring of cyber-physical systems under timing and memory constraints[J].ACM Transactions on Embedded Computing Systems,2015,14(4):79-108.
[6] Yu K,Chen Z,Dong W.Apredictive runtime verification framework for cyber-physical systems[A].IEEE Eighth International Conference on Software Security and Reliability-Companion[C].San Francisco,California,USA:IEEE,2014.223-227.
[7] Bak S,Huang Z,Abad F A T,et al.Safety andprogress for distributed cyber-physical systems with unreliable communication[J].ACM Transactions on Embedded Computing Systems,2015,14(4):1-22.
[8] Mao J,Chen L.Runtimemonitoring for cyber-physical systems:a case study of cooperative adaptive cruise control[A].Second International Conference on Intelligent System Design and Engineering Application[C].Sanya,Hainan,China:IEEE,2012.509-515.
[9] Sistla A P,?efran M,Feng Y,et al.Timely monitoring of partially observable stochastic systems[A].International Conference on Hybrid Systems:Computation and Control[C].Chicago,Illinois,USA:ACM,2014.61-70.
[10] Stoller SD,Bartocci E,Seyster J,et al.Runtime verification with state estimation[A].International Conference on Runtime Verification[C].Berlin Heidelberg:Springer-Verlag,2011.193-207.
[11] Han T,Katoen JP.Counter examples in probabilistic model checking[A].International Conference on Tools and Algorithms for the Construction and Analysis of Systems[C].Berlin Heidelberg:Springer-Verlag,2007.72-86.
[12] Rabiner L.A tutorial onhidden Markov models and selected applications in speech recognition[J].Proceedings of the IEEE,1989,77(2):257-286.
[13] Zhao C,Wu C,Chai J,et al.Decomposition-based multi-objective firefly algorithm for RFID network planning with uncertainty[J].Applied Soft Computing,2017,55(6):549-564.
[14] Amditis A,Bimpas M,Thomaidis G,et al.A situation-adaptive lane-keeping support system:overview of the SAFELANE approach[J].IEEE Transactions on Intelligent Transportation Systems,2010,11(3):617-629.
[15] Kalajdzic K,Bartocci E,Smolka SA,et al.Runtimeverification with particle filtering[A].International Conference on Runtime Verification[C].Berlin Heidelberg:Springer-Verlag,2013.149-166.
2018, Vol. 46 
