在嵌入式软件开发早期,为其建立可靠性模型能够尽早发现软件设计中存在的问题,从而节约嵌入式软件开发成本。AADL从软件结构和故障传播两个角度来建立软件可靠性模型,但是AADL的半形式化性质使得基于AADL建立的可靠性模型难以对可靠性...在嵌入式软件开发早期,为其建立可靠性模型能够尽早发现软件设计中存在的问题,从而节约嵌入式软件开发成本。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]结果的对比说明了所提方法的正确性和有效性。展开更多
文摘在嵌入式软件开发早期,为其建立可靠性模型能够尽早发现软件设计中存在的问题,从而节约嵌入式软件开发成本。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]结果的对比说明了所提方法的正确性和有效性。
