计算机科学 ›› 2019, Vol. 46 ›› Issue (8): 217-223.doi: 10.11896/j.issn.1002-137X.2019.08.036

• 软件与数据库技术 • 上一篇    下一篇

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

李蜜, 庄毅, 胡镡文   

  1. (南京航空航天大学计算机科学与技术学院 南京211106)
  • 收稿日期:2018-07-06 出版日期:2019-08-15 发布日期:2019-08-15
  • 通讯作者: 庄毅(1956-),女,教授,博士生导师,主要研究方向为可信计算、形式化方法,E-mail:zy16@nuaa.edu.cn
  • 作者简介:李蜜(1993-),男,硕士生,主要研究方向为软件可靠性、形式化方法;胡镡文(1994-),女,博士生,主要研究方向为软件安全性、形式化方法
  • 基金资助:
    国家自然科学基金面上项目(61572253),航空基金 XXX 专项(2016ZC52030),“十三五”装备预研领域基金(61402420101HK02001)

Embedded Software Reliability Model and Evaluation Method Combining AADL and Z

LI Mi, ZHUANG Yi, HU Xin-wen   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)
  • Received:2018-07-06 Online:2019-08-15 Published:2019-08-15

摘要: 在嵌入式软件开发早期,为其建立可靠性模型能够尽早发现软件设计中存在的问题,从而节约嵌入式软件开发成本。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, DTMC, Z语言, 可靠性, 嵌入式软件

Abstract: 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.

Key words: AADL, DTMC, Embedded software, Reliability, Z language

中图分类号: 

  • TP311.5
[1]FEILER P H,GLUCH D P,HUDAK J J.The architecture ana- lysis & design language (AADL):An introduction[R].Pittsburgh:Carnegie-Mellon Univ Pittsburgh PA Software Enginee-ring Inst,2006.
[2]LI J Y,CAO Z N.An AADL Modeling Method Based on Concurrency[J].Computer & Modernization,2017(5):1-4.
[3]ZHOU D X,LI N,LIU Z X.Modeling and Analysis of Avionics Configurations Control System Based on AADL[J].Computer Science,2016,43(S1):55-59.
[4]WEI X,DONG Y W,YANG M,et al.Hazard analysis for AADL model[C]∥Proceedings of the 2014 IEEE 20th International Conference on Embedded and Real-Time Computing Systems and Applications.Chongqing,China:IEEE,2014:1-10.
[5]MUNOZ M.Space systems modeling using the Architecture Analysis & Design Language (AADL)[C]∥2013 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW).Pasadena:IEEE,2013:97-98.
[6]YANG Z B,PI L,HU K,et al.AADL:An architecture design and analysis language for complex embedded real-time systems[J].Journal of Software,2010,21(5):899-915.
[7]ZHANG X C,YAN X F,ZHOU Y.A Method for Conversion of AADL Model into Dynamic Fault Tree[J].Computer Technology and Development,2017,27(11):110-114.
[8]LI D M,LI J,LIN H F.Reliability Analysis Method of Embedded System AADL Model Based on Fault Tree Analysis[J].Computer Science,2017,44(6):182-188.
[9]SPIVEY J M,ABRIAL J.The Z notation [M].Hemel Hempstead:Prentice Hall,1992.
[10]SMITH G.The Object-Z specification language[M].New York:Springer Science & Business Media,2012.
[11]LANO K,HAUGHTON H.The z++ manual[M].Lloyds Re- gister of Shipping,1994:29-62.
[12]FISCHER C.CSP-OZ:a combination of Object-Z and CSP[M]∥ Formal Methods for Open Object-based Distributed Systems.Springer,Boston,MA,1997:423-438.
[13]SMITH G,LI Q.Maze:An extension of object-z for multi-agent systems[C]∥International Conference on Abstract State Machines,Alloy,B,TLA,VDM,and Z.Berlin Heidelberg:Sprin-ger,2014:72-85.
[14]NAJAFI M,HAGHIGHI H.An integration of UML-B and object-Z in software development process [J].Lecture Notes in Electrical Engineering,2013,152:633-648.
[15]NI S R,ZHUANG Y,CAO Z N,et al.Modeling dependability features for real-time embedded systems [J].IEEE Transactions on Dependable and Secure Computing,2015,12(2):190-203.
[16]ABRAHAM E,JANSEN N,WIMMER R,et al.DTMC model checking by SCC reduction[C]∥2010 Seventh International Conference on the Quantitative Evaluation of Systems.Williamsburg:IEEE,2010:37-46.
[17]CHENG Y H,HUANG Z Q,KAN S L.A system dependability modeling method using AADL and IMC[J].Computer Engineering & Science,2015,37(8):1517-1524.
[18]BOUDALI H,CROUZEN P,HAVERKORT B,et al.Arcade-A formal,extensible,model-based dependability evaluation framework[C]∥13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2008).Belfast:IEEE,2008:243-248.
[19]GAO Z W.Reliability Modeling and Evaluation of Embedded Software Based on AADL[D].Xi’an:Xidian University,2011.
[1] 王鑫, 周泽宝, 余芸, 陈禹旭, 任昊文, 蒋一波, 孙凌云.
一种面向电能量数据的联邦学习可靠性激励机制
Reliable Incentive Mechanism for Federated Learning of Electric Metering Data
计算机科学, 2022, 49(3): 31-38. https://doi.org/10.11896/jsjkx.210700195
[2] 房婷, 宫傲宇, 张帆, 林艳, 贾林琼, 张一晋.
一种传输时限下认知无线电网络的动态广播策略
Dynamic Broadcasting Strategy in Cognitive Radio Networks Under Delivery Deadline
计算机科学, 2021, 48(7): 340-346. https://doi.org/10.11896/jsjkx.200900001
[3] 亓慧, 史颖, 李灯熬, 穆晓芳, 侯明星.
基于连续型深度置信神经网络的软件可靠性预测
Software Reliability Prediction Based on Continuous Deep Confidence Neural Network
计算机科学, 2021, 48(5): 86-90. https://doi.org/10.11896/jsjkx.210200055
[4] 冯凯, 马鑫玉.
(n,k)-冒泡排序网络的子网络可靠性
Subnetwork Reliability of (n,k)-bubble-sort Networks
计算机科学, 2021, 48(4): 43-48. https://doi.org/10.11896/jsjkx.201100139
[5] 冯凯, 李婧.
k元n方体的子网络可靠性研究
Study on Subnetwork Reliability of k-ary n-cubes
计算机科学, 2020, 47(7): 31-36. https://doi.org/10.11896/jsjkx.190700170
[6] 王慧妍, 徐经纬, 许畅.
环境感知自适应软件的运行时输入验证技术综述
Survey on Runtime Input Validation for Context-aware Adaptive Software
计算机科学, 2020, 47(6): 1-7. https://doi.org/10.11896/jsjkx.200400081
[7] 程煜, 刘伟, 孙童心, 魏志刚, 杜薇.
近阈值电压下可容错的一级缓存结构设计
Design of Fault-tolerant L1 Cache Architecture at Near-threshold Voltage
计算机科学, 2020, 47(4): 42-49. https://doi.org/10.11896/jsjkx.190300088
[8] 丁嵘, 于千惠.
基于AADL的自主无人系统可成长框架
Growth Framework of Autonomous Unmanned Systems Based on AADL
计算机科学, 2020, 47(12): 87-92. https://doi.org/10.11896/jsjkx.201100173
[9] 李苏婷,张严.
GSOS算子下共变-异变模拟的公理刻画
Axiomatizing Covariation-Contravariation Simulation Under GSOS Operators
计算机科学, 2020, 47(1): 51-58. https://doi.org/10.11896/jsjkx.181102026
[10] 弋泽龙,温玉梅,林燕敏,陈伟庭,吕冠宇.
多层缺陷关联效应对软件可靠性增长过程的影响
Impacts of Correlation Effects among Multi-layer Faults on Software Reliability Growth Processes
计算机科学, 2018, 45(2): 241-248. https://doi.org/10.11896/j.issn.1002-137X.2018.02.042
[11] 吴文华, 宋亚飞, 刘晶.
直觉模糊框架内的证据动态可靠性评估及应用
Dynamic Reliability Evaluation Method of Evidence Based on Intuitionistic Fuzzy Sets and Its Applications
计算机科学, 2018, 45(12): 160-165. https://doi.org/10.11896/j.issn.1002-137X.2018.12.025
[12] 刘凯, 梁欣, 张俊萍.
基于软硬系统综合方法的软件失效问题分析
Analysis on Technical Support Equipments’ Software Invalidation Based on Soft and Hard Integrated System Methodology
计算机科学, 2018, 45(11A): 494-496.
[13] 赵冉, 潘根梅.
能量捕获无线传感器网络中高可靠数据收集策略
High Reliable Data Collection Algorithm in Energy Harvesting Wireless Sensor Networks
计算机科学, 2018, 45(11A): 303-307.
[14] 李灵俐, 白光伟, 沈航, 王天荆.
基于簇的认知多媒体传感器网络实时路由协议
Cluster-based Real-time Routing Protocol for Cognitive Multimedia Sensor Networks
计算机科学, 2018, 45(10): 83-88. https://doi.org/10.11896/j.issn.1002-137X.2018.10.016
[15] 欧阳城添,陈莉莉,王曦.
高层次时序电路可靠度估计方法研究进展
Survey on Reliability Estimation Methods of Sequential Circuit in Height-level
计算机科学, 2017, 44(Z11): 33-38. https://doi.org/10.11896/j.issn.1002-137X.2017.11A.006
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!