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.