Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking

Yongxiang Bao, Mingsong Chen*, Qi Zhu, Tongquan Wei, Frederic Mallet, Tingliang Zhou

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

18 Scopus citations


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.

Original languageEnglish (US)
Article number7875425
Pages (from-to)1989-2002
Number of pages14
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number12
StatePublished - Dec 2017


  • Hybrid architecture analysis and design language (AADL)
  • quantitative performance evaluation
  • statistical model checking (SMC)
  • uncertainty

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering


Dive into the research topics of 'Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking'. Together they form a unique fingerprint.

Cite this