| 摘要: |
| 许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system, MCS). MCS通常需要在指定的关键性(criticality)等级状态下运行, 但是它们可能会受到一些危害的影响, 这些危害可能会导致随机错误和突发错误, 进一步导致执行线程中止, 甚至导致系统故障. 目前的研究仅集中于对MCS的可调度性分析, 未能进一步分析系统安全性, 未能考虑线程之间的依赖关系. 以随机错误和突发错误为研究对象, 提出一种集成故障传播分析的基于架构的MCS安全分析方法. 使用架构分析和设计语言(architecture analysis and design language, AADL)刻画构件依赖关系. 为了弥补AADL的不足, 创建新的AADL属性(AADL突发错误属性), 并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程. 为了将概率模型检查应用于安全分析, 提出模型转换规则和组装方法, 从AADL模型推导出PRISM模型. 建立了两个公式, 分别获得定量安全属性以验证故障发生的概率, 以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析. 最后, 以动力艇自动驾驶仪(power boat autopilot, PBA)系统为例, 验证了该方法的有效性. |
| 关键词: 混合关键系统 突发错误 模型转换 安全性分析 概率模型检验 |
| DOI：10.13328/j.cnki.jos.007137 |
| 分类号: |
| 基金项目:国家自然科学基金(62232013, 62272366, 62125205); 中央高校基本科研业务费专项资金(ZYTS23165); 陕西省重点研发计划(2023-YBGY-371) |
|
| Safety Analysis for Mixed-criticality System with Random Errors and Burst Errors Based on AADL |
|
WEI Xiao-Min1, DONG Yun-Wei2, SUN Cong1, LI Xing-Hua1, MA Jian-Feng1
|
|
1.School of Cyber Engineering, Xidian University, Xi’an 710071, China;2.School of Computer Science, Northwestern Polytechnical University, Xi’an 710072, China
|
| Abstract: |
| Many complex embedded systems are mixed-criticality systems (MCSs). MCSs are often required to operate with the specified criticality level, but they may be subject to hazards that can induce random errors and burst errors, which may result in the abortion of an executing thread or even system failures. Current research only concentrates on schedulability analysis for MCSs and fails to further analyze system safety and consider the dependency relationship among threads. Taking random errors and burst errors as the research objects, this study proposes an architecture-based MCS safety analysis method with the integration of fault propagation analysis. Meanwhile, architecture analysis and design language (AADL) is employed to characterize the dependency relations among components. To compensate for the shortcomings of AADL, this study creates new AADL properties (AADL burst error properties) and proposes new thread state machine (burst error-based thread state machine) semantics to describe the thread execution process with burst errors. Additionally, model transformation rules and assembly methods are proposed to apply probabilistic model checking for safety analysis, and PRISM models are derived from AADL models. Two formulae are also formulated to obtain quantitative safety properties for verifying occurrence probabilities of failures, and qualitative safety properties for generating corresponding witnesses to figure out propagation paths for fault propagation analysis respectively. Finally, the effectiveness of the proposed method is verified by adopting a power boat autopilot (PBA) system. |
| Key words: mixed-criticality system burst error model transformation safety analysis probabilistic model checking |
