Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking. Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., & Zhou, T. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 36(12):1989–2002, December, 2017. Conference Name: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systemsdoi abstract bibtex 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.
@article{bao_quantitative_2017,
title = {Quantitative {Performance} {Evaluation} of {Uncertainty}-{Aware} {Hybrid} {AADL} {Designs} {Using} {Statistical} {Model} {Checking}},
volume = {36},
issn = {1937-4151},
doi = {10.1109/TCAD.2017.2681076},
abstract = {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.},
number = {12},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
author = {Bao, Yongxiang and Chen, Mingsong and Zhu, Qi and Wei, Tongquan and Mallet, Frederic and Zhou, Tingliang},
month = dec,
year = {2017},
note = {Conference Name: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
keywords = {Analytical models, Computational modeling, Computer architecture, Hybrid architecture analysis and design language (AADL), Model checking, Ports (Computers), Statistical analysis, Uncertainty, quantitative performance evaluation, statistical model checking (SMC), uncertainty},
pages = {1989--2002},
}
Downloads: 0
{"_id":"36wi73p7G5tn5DepG","bibbaseid":"bao-chen-zhu-wei-mallet-zhou-quantitativeperformanceevaluationofuncertaintyawarehybridaadldesignsusingstatisticalmodelchecking-2017","author_short":["Bao, Y.","Chen, M.","Zhu, Q.","Wei, T.","Mallet, F.","Zhou, T."],"bibdata":{"bibtype":"article","type":"article","title":"Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking","volume":"36","issn":"1937-4151","doi":"10.1109/TCAD.2017.2681076","abstract":"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.","number":"12","journal":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","author":[{"propositions":[],"lastnames":["Bao"],"firstnames":["Yongxiang"],"suffixes":[]},{"propositions":[],"lastnames":["Chen"],"firstnames":["Mingsong"],"suffixes":[]},{"propositions":[],"lastnames":["Zhu"],"firstnames":["Qi"],"suffixes":[]},{"propositions":[],"lastnames":["Wei"],"firstnames":["Tongquan"],"suffixes":[]},{"propositions":[],"lastnames":["Mallet"],"firstnames":["Frederic"],"suffixes":[]},{"propositions":[],"lastnames":["Zhou"],"firstnames":["Tingliang"],"suffixes":[]}],"month":"December","year":"2017","note":"Conference Name: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","keywords":"Analytical models, Computational modeling, Computer architecture, Hybrid architecture analysis and design language (AADL), Model checking, Ports (Computers), Statistical analysis, Uncertainty, quantitative performance evaluation, statistical model checking (SMC), uncertainty","pages":"1989–2002","bibtex":"@article{bao_quantitative_2017,\n\ttitle = {Quantitative {Performance} {Evaluation} of {Uncertainty}-{Aware} {Hybrid} {AADL} {Designs} {Using} {Statistical} {Model} {Checking}},\n\tvolume = {36},\n\tissn = {1937-4151},\n\tdoi = {10.1109/TCAD.2017.2681076},\n\tabstract = {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.},\n\tnumber = {12},\n\tjournal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n\tauthor = {Bao, Yongxiang and Chen, Mingsong and Zhu, Qi and Wei, Tongquan and Mallet, Frederic and Zhou, Tingliang},\n\tmonth = dec,\n\tyear = {2017},\n\tnote = {Conference Name: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},\n\tkeywords = {Analytical models, Computational modeling, Computer architecture, Hybrid architecture analysis and design language (AADL), Model checking, Ports (Computers), Statistical analysis, Uncertainty, quantitative performance evaluation, statistical model checking (SMC), uncertainty},\n\tpages = {1989--2002},\n}\n\n","author_short":["Bao, Y.","Chen, M.","Zhu, Q.","Wei, T.","Mallet, F.","Zhou, T."],"key":"bao_quantitative_2017","id":"bao_quantitative_2017","bibbaseid":"bao-chen-zhu-wei-mallet-zhou-quantitativeperformanceevaluationofuncertaintyawarehybridaadldesignsusingstatisticalmodelchecking-2017","role":"author","urls":{},"keyword":["Analytical models","Computational modeling","Computer architecture","Hybrid architecture analysis and design language (AADL)","Model checking","Ports (Computers)","Statistical analysis","Uncertainty","quantitative performance evaluation","statistical model checking (SMC)","uncertainty"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"https://api.zotero.org/groups/4682325/items?key=gQcofis3fp4rTPEF0VitS7qe&format=bibtex&limit=100","dataSources":["rbZEZqmLz8K8iv4Hi"],"keywords":["analytical models","computational modeling","computer architecture","hybrid architecture analysis and design language (aadl)","model checking","ports (computers)","statistical analysis","uncertainty","quantitative performance evaluation","statistical model checking (smc)","uncertainty"],"search_terms":["quantitative","performance","evaluation","uncertainty","aware","hybrid","aadl","designs","using","statistical","model","checking","bao","chen","zhu","wei","mallet","zhou"],"title":"Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking","year":2017}