Research On AADL-based Reliability Modeling And Evaluation Technology Of Embedded Software

Nowadays,reliability requirements of embedded software are becoming higher and higher as they have been widely used in security-critical areas such as aerospace and industrial control.Meanwhile,as embedded software showing a development trend of becoming more complicated,larger in scale and more open,it has become one of the research hotspots for researchers,both at home and abroad,to study on how to ensure high software reliability.Through analyzing,verifying and evaluating software reliability specifications at the early development stage,potential flaws can be reduced,and thus lower the cost of testing and maintenance.Based on the formal semantics of Z notation,this thesis aims at exploring the basic theory and methodology for modeling and evaluating embedded software reliability.The effectiveness of the proposed methodology is validated through case studies on an implemented prototype system.The main research work of this thesis can be summarized as follows:(1)An extensible reliability model Z-AADL for embedded software is proposed,including Z-AADL error model,structure model and behavior model.Compared with the existing models,Z-AADL is an integrated model that combines static structure and dynamic behavior.With a good extensibility,Z-AADL can describe the architecture and error behavior of the embedded software.(2)In order to evaluate the reliability described by Z-AADL model,an evaluation method of Z-AADL based on model checking technology is proposed.Firstly,the Z-AADL model is characterized as a discrete-time Markov chain DTMC to describe the state transition relations of the embedded software.A temporal logic PCTL is used to describe the reliability.Then,a reliability evaluation algorithm ZARE based on PCTL formula is proposed,to calculate PCTL formula and to obtain the reliability evaluation result.(3)Based on the above research results,a prototype system of embedded software reliability modeling and evaluation is established.XSLT interpreter is integrated into the OSATE platform to build the Z-AADL model.A reliability evaluator is designed and implemented on VS2008 platform,including parser module of DTMC and ZARE algorithm module.Finally,a case study of flight management system is given to illustrate the modeling and evaluation processes.