一种结合AADL与Z的嵌入式软件可靠性建模与评估方法  

Embedded Software Reliability Model and Evaluation Method Combining AADL and Z

作　　者：李蜜[1] 庄毅[1] 胡镡文 LI Mi;ZHUANG Yi;HU Xin-wen(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院

出　　处：《计算机科学》2019年第8期217-223,共7页Computer Science

基　　金：国家自然科学基金面上项目(61572253);航空基金XXX专项(2016ZC52030);“十三五”装备预研领域基金(61402420101HK02001)资助

摘　　要：在嵌入式软件开发早期,为其建立可靠性模型能够尽早发现软件设计中存在的问题,从而节约嵌入式软件开发成本。AADL从软件结构和故障传播两个角度来建立软件可靠性模型,但是AADL的半形式化性质使得基于AADL建立的可靠性模型难以对可靠性、安全性等非功能属性进行严格的分析与验证。形式规格说明语言Z语言具有很强的逻辑描述能力,能够精确表达软件中的各种约束,这使得基于Z语言建立的可靠性模型能够很好地进行严格的分析和验证。因此,考虑到AADL和Z的特征,文中提出了一种将AADL与Z相结合的形式化可靠性模型(embedded software Reliability Model combined with Z and AADL,ZARM),该模型具有AADL的描述能力和Z的精确性。文中给出了ZARM故障模型、结构模型和行为模型的建模方法,并在谓词中描述了与可靠性相关的数据约束。在ZARM模型的基础上,文中提出了一种面向概率的基于DTMC的可靠性评估方法,来对ZARM模型进行可靠性定量评估和分析。最后,通过一个飞行管理系统对应用ZARM模型进行可靠性建模的过程进行了说明,并采用所提评估方法对其进行了可靠性评估。评估结果与文献[19]结果的对比说明了所提方法的正确性和有效性。In the early stage of embedded software development,a reliability model is established for it to discover problems in software design as early as possible,thereby saving embedded software development costs.AADL establishes software reliability model from two aspects of software structure and fault propagation.However,the semi-formal nature of AADL makes it difficult to analyze and verify the non-functional attributes such as reliability and security.The formal specification language Z language has a strong logical description ability and can accurately express various constraints in the software,which makes the reliability model based on the Z language well rigorously analyzed and verified.Therefore,considering the characteristics of AADL and Z,an embedded software reliability model combined with Z and AADL(ZARM)was proposed.The modeling methods of ZARM fault model,structure model and behavior model were given,and the data constraints related to reliability were described in the predicate.Based on the ZARM model,a probabilistic DTMC-based reliability evaluation method was proposed to quantitatively evaluate and analyze the ZARM model.Finally,the process of reliability modeling using ZARM model was described by a flight management system(FMS),and the reliability evaluation was carried out by using the proposed evaluation method.The comparison between the evaluation results and the reference[19]results shows the correctness and effectiveness of the proposed method.

关 键 词：嵌入式软件 可靠性 AADL Z语言 DTMC 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]