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

Abstract : — Architecture Analysis and Design Language (AADL) is widely used for the architecture design and analysis of safety-critical real-time systems. Based on the Hybrid annex which supports continuous behavior modeling, Hybrid AADL enables seamless interactions between embedded control systems and continuous physical environments. Although Hybrid AADL is promising in dependability prediction through analyzable architecture development, the worst-case performance analysis of Hybrid AADL designs can easily lead to an overly pessimistic estimation. So far, Hybrid AADL cannot be used to accurately quantify and reason the overall performance of complex systems which interact with external uncertain environments intensively. To address this problem, 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 (NPTA) and performance queries, respectively. Comprehensive experimental results on the Movement Authority (MA) scenario of Chinese Train Control System Level 3 (CTCS-3) demonstrate the effectiveness of our approach.
Document type :
Journal articles
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01644285
Contributor : Frédéric Mallet <>
Submitted on : Wednesday, November 22, 2017 - 9:52:55 AM
Last modification on : Wednesday, August 7, 2019 - 12:16:27 PM

File

AADL.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Yongxiang Bao, Mingsong Chen, Qi Zhu, Tongquan Wei, Tingliang Zhou, et al.. Quantitative Performance Evaluation of Uncertainty-Aware Hybrid AADL Designs Using Statistical Model Checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, IEEE, 2017, 36 (12), pp.1989 - 2002. ⟨10.1109/TCAD.2017.2681076⟩. ⟨hal-01644285⟩

Share

Metrics

Record views

513

Files downloads

188