基于AADL的混合关键系统随机错误与突发错误安全性分析

许多复杂的嵌入式系统都是混合关键系统(mixed-criticality system,简称MCS).MCS通常需要在指定的关键性(criticality)等级状态下运行,但是它们可能会受到一些危害的影响,这些危害可能会导致随机错误和突发错误,进一步导致执行线程中止,甚至导致系统故障.目前的研究仅集中于对MCS的可调度性分析,未能进一步分析系统安全性,未能考虑线程之间的依赖关系.本文以随机错误和突发错误为研究对象,提出一种集成故障传播分析的基于架构的MCS安全分析方法.使用架构分析和设计语言(Architecture Analysis and Design Language,简称AADL)刻画构件依赖关系.为了弥补AADL的不足,创建新的AADL属性(AADL突发错误属性),并提出新的线程状态机(突发错误行为线程状态机)语义来描述带有突发错误的线程执行过程.为了将概率模型检查应用于安全分析,提出模型转换规则和组装方法,从AADL模型推导出PRISM模型.建立了两个公式,分别获得定量安全属性以验证故障发生的概率,以及定性安全属性以生成相应的正例来求出故障传播路径来进行故障传播分析.最后,以动力艇自动驾驶仪(power boat autopilot,简称PBA)系统为例,验证了该方法的有效性.

Safety Analysis for Mixed-criticality Systems with Random Errors and Error Bursts Based on AADL

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 error bursts, which may result in the abortion of an executing thread or even lead to system failures. Current research only concentrates on schedulability analysis for MCSs, and fails to further analyze system safety and consider the dependency relationship between threads. This paper focuses on random errors and error bursts, and proposes an architecture-based safety analysis approach with the integration of fault propagation analysis. The component dependency relationship is specified using Architecture Analysis and Design Language (AADL). To compensate AADL, we create new AADL properties (AADL error burst properties) and establish new thread state machine (error burst-based thread state machine) semantics to describe thread execution process with error bursts. To apply probabilistic model checking for safety analysis, model transformation rules and assembly methods are made to derive PRISM models 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, we demonstrate the effectiveness using a power boat autopilot (PBA) system.