TY - JOUR
T1 - Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking
AU - Bao, Yongxiang
AU - Chen, Mingsong
AU - Zhu, Qi
AU - Wei, Tongquan
AU - Mallet, Frederic
AU - Zhou, Tingliang
N1 - Funding Information:
Manuscript received September 29, 2016; revised January 1, 2017; accepted February 19, 2017. Date of publication March 10, 2017; date of current version November 20, 2017. This work was supported in part by the Natural Science Foundation of China under Grant 61672230 and Grant 91418203, in part by the Shanghai Municipal NSF under Grant 16ZR1409000, and in part by the National Science Foundation of United States under Grant CCF-1553757 and Grant CCF-1646381. This paper was recommended by Associate Editor T. Mitra. (Corresponding author: Mingsong Chen.) Y. Bao, M. Chen, and T. Wei are with the Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China (e-mail: mschen@sei.ecnu.edu.cn).
Funding Information:
This work was supported in part by the Natural Science Foundation of China under Grant 61672230 and Grant 91418203, in part by the Shanghai Municipal NSF under Grant 16ZR1409000, and in part by the National Science Foundation of United States under Grant CCF-1553757 and Grant CCF-1646381.
Publisher Copyright:
© 1982-2012 IEEE.
PY - 2017/12
Y1 - 2017/12
N2 - The hybrid architecture analysis and design language (AADL) has been proposed to model the interactions between embedded control systems and continuous physical environment. However, the worst-case performance analysis of hybrid AADL designs often leads to overly pessimistic estimations, and is not suitable for accurate reasoning about overall system performance, in particular when the system closely interacts with an uncertain external environment. To address this challenge, this paper proposes a statistical model checking-based framework that can perform quantitative evaluation of uncertainty-aware hybrid AADL designs against various performance queries. Our approach extends hybrid AADL to support the modeling of environment uncertainties. Furthermore, we propose a set of transformation rules that can automatically translate AADL designs together with designers' requirements into networks of priced timed automata and performance queries, respectively. Comprehensive experimental results on the movement authority scenario of Chinese train control system level 3 demonstrate the effectiveness of our approach.
AB - The hybrid architecture analysis and design language (AADL) has been proposed to model the interactions between embedded control systems and continuous physical environment. However, the worst-case performance analysis of hybrid AADL designs often leads to overly pessimistic estimations, and is not suitable for accurate reasoning about overall system performance, in particular when the system closely interacts with an uncertain external environment. To address this challenge, this paper proposes a statistical model checking-based framework that can perform quantitative evaluation of uncertainty-aware hybrid AADL designs against various performance queries. Our approach extends hybrid AADL to support the modeling of environment uncertainties. Furthermore, we propose a set of transformation rules that can automatically translate AADL designs together with designers' requirements into networks of priced timed automata and performance queries, respectively. Comprehensive experimental results on the movement authority scenario of Chinese train control system level 3 demonstrate the effectiveness of our approach.
KW - Hybrid architecture analysis and design language (AADL)
KW - quantitative performance evaluation
KW - statistical model checking (SMC)
KW - uncertainty
UR - http://www.scopus.com/inward/record.url?scp=85040662057&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85040662057&partnerID=8YFLogxK
U2 - 10.1109/TCAD.2017.2681076
DO - 10.1109/TCAD.2017.2681076
M3 - Article
AN - SCOPUS:85040662057
VL - 36
SP - 1989
EP - 2002
JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
SN - 0278-0070
IS - 12
M1 - 7875425
ER -