一种嵌入式软件可靠性建模与评估方法

doi:10.3969/j.issn.1006-2475.2017.08.017

计算机与现代化

一种嵌入式软件可靠性建模与评估方法

南京航空航天大学计算机科学与技术学院，江苏南京210016

收稿日期:2016-12-17 出版日期:2017-08-31 发布日期:2017-09-01
作者简介:刘维维（1991-），男，江苏如皋人，南京航空航天大学计算机科学与技术学院硕士研究生，研究方向：软件可靠性，形式化方法；庄毅（1956-），女，教授，博士生导师，研究方向：可信计算；李蜜（1993-），男，硕士研究生，研究方向：软件可靠性，形式化方法。
基金资助:
国家自然科学基金资助面上项目(61572253)

An Embedded Software Reliability Modeling and Evaluation Method

College of Information Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China

Received:2016-12-17 Online:2017-08-31 Published:2017-09-01

摘要/Abstract

摘要：

虽然AADL已经被广泛应用于嵌入式软件体系结构的建模与分析，但其作为一种半形式化建模语言，不能满足严格分析评估软件可靠性的要求。为了解决这个问题，本文首先采用离散时间马尔可夫

链DTMC刻画AADL可靠性模型，主要描述系统的状态转移与转移概率。然后基于概率计算树逻辑PCTL提出一种可靠性定量评估方法，通过计算可用度评估可靠性。最后设计可靠性评估器，并通过一个飞行

管理系统的实例研究验证所提出的建模与评估方法的有效性。

关键词: , 可靠性, 体系结构分析与设计语言, 离散时间马尔可夫链, 概率计算树逻辑, 模型检测

Abstract:

Although AADL has been widely used in the modeling and analysis of embedded software architecture, it’s a semiformal modeling language and cannot meet the

requirements of rigorous analysis and evaluation of software reliability. In order to solve this problem, first of all, we describe the AADL reliability model by discretetime

Markov chain, which is mainly used to describe the state transition and transition probability of the system. Then, we propose a reliability quantitative evaluation method based

on PCTL to evaluate the reliability by calculating the availability. Finally, we design a reliability evaluation tool. By the tool, a case study of a flight management system is

given to verify the effectiveness of the modeling and evaluation method.


Key words: reliability, AADL, DTMC, PCTL, model checking

中图分类号:

TP311.5

刘维维，庄毅，李蜜. 一种嵌入式软件可靠性建模与评估方法[J]. 计算机与现代化, doi: 10.3969/j.issn.1006-2475.2017.08.017.

LIU Weiwei, ZHUANG Yi, LI Mi. An Embedded Software Reliability Modeling and Evaluation Method[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2017.08.017.

［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.

[1]	姜厚海, 庄毅, 曹子宁. 一种基于改进BDD的SDN可靠性评估算法[J]. 计算机与现代化, 2023, 0(09): 64-69.
[2]	王颖颖, 庄毅, 孙逸帆. 基于粒子群优化BP神经网络的可靠性评估模型[J]. 计算机与现代化, 2022, 0(12): 42-49.
[3]	李静元, 张珂, 杨东裕. 基于雾计算的工业互联网安全数据访问方法[J]. 计算机与现代化, 2022, 0(12): 118-122.
[4]	陈春燕, 刘梦赤. 基于粒子群遗传算法的智能组卷策略[J]. 计算机与现代化, 2021, 0(08): 16-23.
[5]	宋鑫, 樊志强, . 基于Laguerre 前向神经网络的信息服务性能建模方法 [J]. 计算机与现代化, 2021, 0(03): 1-6.
[6]	魏健, 赵红涛, 刘敦楠, 加鹤萍 . 基于集成模型的超短时负荷预测方法[J]. 计算机与现代化, 2021, 0(03): 12-17.
[7]	杨牧川, 吕晓丹, 蒋朝惠, . 云计算环境下的可修分布式系统可靠性分析方法[J]. 计算机与现代化, 2020, 0(06): 28-.
[8]	李思雨 . 基于极限学习机的组合软件可靠性模型研究[J]. 计算机与现代化, 2019, 0(11): 44-.
[9]	韦海龙,孙宁,张杰,武张. 水声传感网中基于网络编码的协作传输算法[J]. 计算机与现代化, 2019, 0(06): 24-.
[10]	王关祥,李义勇,夏亚东,王志献. 基于多层次评价模型的高校网络运行可靠性分析[J]. 计算机与现代化, 2019, 0(06): 98-.
[11]	段桂芹1，邹臣嵩2，刘锋2. 基于优化初始聚类中心的K中心点算法[J]. 计算机与现代化, 2019, 0(04): 1-.
[12]	肖楚琬1，邓力2，张真3. 无失效数据机载多余度EWIS可靠性研究[J]. 计算机与现代化, 2019, 0(04): 98-.
[13]	李富星，蒙祖强 . 一种改进的类别区分词特征选择算法[J]. 计算机与现代化, 2019, 0(03): 73-.
[14]	郭鑫，闫连山，李洪赭，张晓薇. 基于SD-WSN的高危仓储无线监测系统[J]. 计算机与现代化, 2018, 0(10): 84-.
[15]	白晓波1，邵景峰1，和征1，田建刚2. 基于学习的核偏最小二乘法优化扩展卡尔曼滤波[J]. 计算机与现代化, 2018, 0(09): 110-.

一种嵌入式软件可靠性建模与评估方法

An Embedded Software Reliability Modeling and Evaluation Method

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价