TY - JOUR
T1 - Scenario-Based Online Reachability Validation for CPS Fault Prediction
AU - Bu, Lei
AU - Wang, Qixin
AU - Ren, Xinyue
AU - Xing, Shaopeng
AU - Li, Xuandong
N1 - Funding Information:
Manuscript received September 19, 2018; revised January 21, 2019 and May 28, 2019; accepted July 12, 2019. Date of publication August 13, 2019; date of current version September 18, 2020. The work of L. Bu, X. Ren, S. Xing, and X. Li was supported in part by the National Key Research and Development Plan under Grant 2017YFA0700604, and in part by the National Natural Science Foundation of China under Grant 61632015, Grant 61572249, and Grant 61561146394. The work of Q. Wang was supported in part by the Hong Kong Research Grants Council (RGC) GRF under Grant PolyU 152002/18E, and Grant PolyU 152164/14E, in part by RGC Germany/HK Joint Research Scheme under Grant G-PolyU503/16, and in part by the Hong Kong Polytechnic University fund under Grant P0009706 (G-YBXW), Grant P0009367 (G-YBMW), Grant P0010792 (G-YN37), Grant P0000157 (1-BBWC), Grant P0013879 (1-BBWH), Grant P0001888 (4-ZZHD), and Grant P0008501 (G-UA7L). This article was recommended by Associate Editor Q. Zhu. (Corresponding author: Lei Bu.) L. Bu, X. Ren, S. Xing, and X. Li are with the State Key Laboratory of Novel Software Technology, Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China (e-mail: [email protected]).
Publisher Copyright:
© 1982-2012 IEEE.
PY - 2020/10
Y1 - 2020/10
N2 - Unlike standalone embedded devices, behaviors of a cyber-physical system (CPS) are highly dynamic. Many parameter values (e.g., those related to nature environment and third party black box functions) are unknown offline. Furthermore, distributed sub-CPSs may exchange data online. In this article, we first propose the concept of parametric hybrid automata (PHA) to describe such complex CPSs. As some PHA parameter values are unknown until runtime, conventional offline model checking is infeasible. Instead, we propose to carry out PHA model checking online, as a fault prediction mechanism. However, this usage is challenged by the high time cost of state reachability verification, which is the conventional focus of model checking. To address this challenge, we propose that the model checking shall focus on online scenario reachability validation instead. Furthermore, we propose a mechanism to compose/decompose scenarios. Our scenario reachability validation can exploit linear programming to achieve polynomial time cost. Evaluations on a state-of-the-art train control system show that our approach can cut online model checking time cost from over 1 h to within 200 ms.
AB - Unlike standalone embedded devices, behaviors of a cyber-physical system (CPS) are highly dynamic. Many parameter values (e.g., those related to nature environment and third party black box functions) are unknown offline. Furthermore, distributed sub-CPSs may exchange data online. In this article, we first propose the concept of parametric hybrid automata (PHA) to describe such complex CPSs. As some PHA parameter values are unknown until runtime, conventional offline model checking is infeasible. Instead, we propose to carry out PHA model checking online, as a fault prediction mechanism. However, this usage is challenged by the high time cost of state reachability verification, which is the conventional focus of model checking. To address this challenge, we propose that the model checking shall focus on online scenario reachability validation instead. Furthermore, we propose a mechanism to compose/decompose scenarios. Our scenario reachability validation can exploit linear programming to achieve polynomial time cost. Evaluations on a state-of-the-art train control system show that our approach can cut online model checking time cost from over 1 h to within 200 ms.
KW - Communication-based train control (CBTC) cyber-physical system (CPS)
KW - linear hybrid automata (LHA)
KW - online modeling and verification
KW - scenario reachability validation
UR - http://www.scopus.com/inward/record.url?scp=85070967030&partnerID=8YFLogxK
U2 - 10.1109/TCAD.2019.2935062
DO - 10.1109/TCAD.2019.2935062
M3 - Journal article
AN - SCOPUS:85070967030
SN - 0278-0070
VL - 39
SP - 2081
EP - 2094
JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
IS - 10
M1 - 8796362
ER -