关键词: AADL, 可靠性模型, IMC模型转换, 形式化方法

Abstract:

As embedded software is widely used in safety-critical areas, its scale, complexity and performance demand increase，so system reliability becomes increasingly important. Architecture analysis and design language (AADL) is an important way for architecture modeling, analysis, and verification in the field of embedded systems and it has gradually become the industry standard. Because AADL is not a full formal model, accurate description of its semantics is required to do quantitative analysis. In this paper we propose an AADLbased software system reliability modeling and evaluation framework. We generate an AADL dependability model based on the AADL model and the AADL error model. The basic elements and the special elements (e.g. error propagation) of the AADL dependability model are transformed into the interactive Markov chains (IMC) model by applying model transformation rules and the resulting IMC quantitative analysis is conducted. The modeling approach is applied to a subsystem of the French Air Traffic Control System, and its feasibility and effectiveness are proved.

Key words: AADL；dependability model；IMC model transformation；formal method