［1］ 褚文奎,张凤鸣,樊晓光. 综合模块化航空电子系统软件体系结构综述［J］. 航空学报, 2009,30(10):1912-1917.
［2］ Feiler P H, Gluch D P, Hudak J J. The Architecture Analysis & Design Language (AADL): An Introduction［R］. CarnegieMellon University Pittsburgh PA Software Engineering,

2006.
［3］ Feiler P H, Gluch D P. Modelbased Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language［M］. AddisonWesley, 2012.
［4］ Bae K, lveczky P C, Meseguer J. Definition, semantics, and analysis of multirate synchronous AADL［C］// International Symposium on Formal Methods. Springer

International Publishing, 2014:94-109.
［5］ Delange J, Feiler P. Architecture fault modeling with the aadl errormodel annex［C］// 2014 40th EUROMICRO Conference on Software Engineering and Advanced Applications.

IEEE, 2014:361-368.
［6］ Vestal S. An overview of the architecture analysis & design language (AADL) error model annex［C］// AADL Workshop. 2005.
［7］ Sun H, Hauptman M, Lutz R. Integrating productline fault tree analysis into AADL models［C］// Proceedings of IEEE the 10th High Assurance Systems Engineering Symposium(

HASE07). 2007:15-22.
［8］ 董云卫,王广仁,张凡,等. AADL模型可靠性分析评估工具［J］. 软件学报, 2011,22(6):1252-1266.
［9］ Hansson H, Jonsson B. A logic for reasoning about time and reliability［J］. Formal Aspects of Computing, 1994,6(5):512-535.
［10］Baier C, Katoen J P, Larsen K G. Principles of Model Checking［M］. MIT press, 2008.
［11］Kattenbelt M, Kwiatkowska M, Norman G, et al. A gamebased abstractionrefinement framework for Markov decision processes［J］. Formal Methods in System Design,

2010,36(3):246-280.
［12］程亦涵,黄志球,阚双龙. 一种结合AADL和IMC的系统可靠性建模方法［J］. 计算机工程与科学, 2015,37(8):1517-1524.
［13］Boudali H, Crouzen P, Haverkort B, et al. ArcadeA formal, extensible, modelbased dependability evaluation framework［C］// Proceedings of the 13th IEEE International

Conference on Engineering of Complex Computer Systems. 2008.
［14］SAE AS5506/3 (Draft), Architecture Analysis and Design Language (AADL) Annex Volume 3: Annex E: Error Model V2 Annex［S］.
［15］Yang Jinji, Su Kaile, Luo Xiangyu, et al. Optimization of bounded model checking［J］. Journal of Software, 2009,20(8):2005-2014.
［16］Zhang Wenhui. Model checking with SATbased characterization of ACTL formulas［C］// International Conference on Formal Engineering Methods. Springer Berlin Heidelberg,

2007,4789:191-211.
［17］毛良文,徐亮. 基于SMT的PTACTL限界模型检测方法［J］. 计算机与现代化, 2016(3):41-45.
［18］周从华,刘志锋,王昌达. 概率计算树逻辑的限界模型检测［J］. 软件学报, 2012,23(7):1656-1668.
［19］高志伟. 基于AADL的嵌入式软件可靠性建模与评估［D］. 西安:西安电子科技大学, 2011.