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.
| Original language | English (US) |
|---|---|
| Article number | 7875425 |
| Pages (from-to) | 1989-2002 |
| Number of pages | 14 |
| Journal | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
| Volume | 36 |
| Issue number | 12 |
| DOIs | |
| State | Published - Dec 2017 |
Funding
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: [email protected]). 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.
Keywords
- 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