TY - GEN
T1 - Uncertainty modeling and quantitative evaluation of cyber-physical systems
AU - Yang, Chenchen
AU - Sun, Haiying
AU - Liu, Jing
AU - Kang, Jiexiang
AU - Yin, Wei
AU - Wang, Hui
AU - Li, Tengfei
N1 - Publisher Copyright:
© 2021 IEEE.
PY - 2021/7
Y1 - 2021/7
N2 - Cyber-physical System (CPS) represents a system that tightly integrates computation, communication, and physical processes. As an effective modeling language, AADL is often applied for real-time and embedded systems. However, AADL has limitations in modeling stochastic events because the interaction between the system and an uncertain external environment is often complex and unpredictable. In this paper, we propose a stochastic hybrid modeling language based on AADL, called SHML. SHML supports both continuous behavior analysis and probabilistic modeling of CPSs. To achieve the verification objective, we present a set of mapping rules to transform the SHML design into networks of stochastic hybrid automata (NSHA). By using statistical model-checking techniques, the obtained NSHA model and performance queries are jointly applied to evaluate the quantitative performance of SHML designs. Experiments on traffic collision avoidance systems are conducted, and the results demonstrate the usability and effectiveness of our approach.
AB - Cyber-physical System (CPS) represents a system that tightly integrates computation, communication, and physical processes. As an effective modeling language, AADL is often applied for real-time and embedded systems. However, AADL has limitations in modeling stochastic events because the interaction between the system and an uncertain external environment is often complex and unpredictable. In this paper, we propose a stochastic hybrid modeling language based on AADL, called SHML. SHML supports both continuous behavior analysis and probabilistic modeling of CPSs. To achieve the verification objective, we present a set of mapping rules to transform the SHML design into networks of stochastic hybrid automata (NSHA). By using statistical model-checking techniques, the obtained NSHA model and performance queries are jointly applied to evaluate the quantitative performance of SHML designs. Experiments on traffic collision avoidance systems are conducted, and the results demonstrate the usability and effectiveness of our approach.
KW - Cyber-physical system (CPS)
KW - Statistical model checking (SMC)
KW - Stochastic hybrid modeling language (SHML)
KW - Traffic collision avoidance systems
KW - Uncertainty
UR - https://www.scopus.com/pages/publications/85115840032
U2 - 10.1109/COMPSAC51774.2021.00120
DO - 10.1109/COMPSAC51774.2021.00120
M3 - 会议稿件
AN - SCOPUS:85115840032
T3 - Proceedings - 2021 IEEE 45th Annual Computers, Software, and Applications Conference, COMPSAC 2021
SP - 874
EP - 883
BT - Proceedings - 2021 IEEE 45th Annual Computers, Software, and Applications Conference, COMPSAC 2021
A2 - Chan, W. K.
A2 - Claycomb, Bill
A2 - Takakura, Hiroki
A2 - Yang, Ji-Jiang
A2 - Teranishi, Yuuichi
A2 - Towey, Dave
A2 - Segura, Sergio
A2 - Shahriar, Hossain
A2 - Reisman, Sorel
A2 - Ahamed, Sheikh Iqbal
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 45th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2021
Y2 - 12 July 2021 through 16 July 2021
ER -