Computer Science ›› 2019, Vol. 46 ›› Issue (8): 217-223.doi: 10.11896/j.issn.1002-137X.2019.08.036

• Software & Database Technology • Previous Articles     Next Articles

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

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: Embedded software, Reliability, AADL, Z language, DTMC

CLC Number: 

  • 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] FENG Kai, LI Jing. Study on Subnetwork Reliability of k-ary n-cubes [J]. Computer Science, 2020, 47(7): 31-36.
[2] WANG Hui-yan, XU Jing-wei, XU Chang. Survey on Runtime Input Validation for Context-aware Adaptive Software [J]. Computer Science, 2020, 47(6): 1-7.
[3] CHENG Yu, LIU Wei, SUN Tong-xin, WEI Zhi-gang, DU Wei. Design of Fault-tolerant L1 Cache Architecture at Near-threshold Voltage [J]. Computer Science, 2020, 47(4): 42-49.
[4] ZHANG Zheng-lin,ZHANG Li-wei,WANG Wen-juan,XIA Li,FU Hao,WANG Hong-zhi,YANG Li-zhuang and
LI Hai. Survey on Computerized Neurocognitive Assessment System [J]. Computer Science, 2020, 47(2): 150-156.
[5] DING Rong, YU Qian-hui. Growth Framework of Autonomous Unmanned Systems Based on AADL [J]. Computer Science, 2020, 47(12): 87-92.
[6] ZHAI Yong, LIU Jin, CHEN Jie, LIU Lei, XING Xu-chao, DU Jiang. Analysis on Mathematical Models of Maintenance Decision and Efficiency Evaluation of Computer Hardware [J]. Computer Science, 2018, 45(6A): 568-572.
[7] YI Ze-long, WEN Yu-mei, LIN Yan-min, CHEN Wei-ting and LV Guan-yu. Impacts of Correlation Effects among Multi-layer Faults on Software Reliability Growth Processes [J]. Computer Science, 2018, 45(2): 241-248.
[8] WU Wen-hua, SONG Ya-fei, LIU Jing. Dynamic Reliability Evaluation Method of Evidence Based on Intuitionistic Fuzzy Sets and Its Applications [J]. Computer Science, 2018, 45(12): 160-165.
[9] ZHAO Ran, PAN Gen-mei. High Reliable Data Collection Algorithm in Energy Harvesting Wireless Sensor Networks [J]. Computer Science, 2018, 45(11A): 303-307.
[10] LIU Kai, LIANG Xin, ZHANG Jun-ping. Analysis on Technical Support Equipments’ Software Invalidation Based on Soft and Hard Integrated System Methodology [J]. Computer Science, 2018, 45(11A): 494-496.
[11] LI Ling-li, BAI Guang-wei, SHEN Hang, WANG Tian-jing. Cluster-based Real-time Routing Protocol for Cognitive Multimedia Sensor Networks [J]. Computer Science, 2018, 45(10): 83-88.
[12] YAN Hong. Research and Application of Multi-objective Optimization Algorithm Based on Interval Reliability Lower Bound [J]. Computer Science, 2017, 44(Z11): 577-579.
[13] OUYANG Cheng-tian, CHEN Li-li and WANG Xi. Survey on Reliability Estimation Methods of Sequential Circuit in Height-level [J]. Computer Science, 2017, 44(Z11): 33-38.
[14] LI Dong-min, LI Jing and LIN Hua-feng. Reliability Analysis Method of Embedded System AADL Model Based on Fault Tree Analysis [J]. Computer Science, 2017, 44(6): 182-188.
[15] CUI Tie-jun, LI Sha-sha and WANG Lai-gui. Multi-attribute Decision Making Model Based on Attribute Circle and Application of Reliability Analysis [J]. Computer Science, 2017, 44(5): 111-115.
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75 .
[2] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[3] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[4] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[5] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99 .
[6] ZHOU Yan-ping and YE Qiao-lin. L1-norm Distance Based Least Squares Twin Support Vector Machine[J]. Computer Science, 2018, 45(4): 100 -105 .
[7] LIU Bo-yi, TANG Xiang-yan and CHENG Jie-ren. Recognition Method for Corn Borer Based on Templates Matching in Muliple Growth Periods[J]. Computer Science, 2018, 45(4): 106 -111 .
[8] GENG Hai-jun, SHI Xin-gang, WANG Zhi-liang, YIN Xia and YIN Shao-ping. Energy-efficient Intra-domain Routing Algorithm Based on Directed Acyclic Graph[J]. Computer Science, 2018, 45(4): 112 -116 .
[9] CUI Qiong, LI Jian-hua, WANG Hong and NAN Ming-li. Resilience Analysis Model of Networked Command Information System Based on Node Repairability[J]. Computer Science, 2018, 45(4): 117 -121 .
[10] WANG Zhen-chao, HOU Huan-huan and LIAN Rui. Path Optimization Scheme for Restraining Degree of Disorder in CMT[J]. Computer Science, 2018, 45(4): 122 -125 .