Research On Dependability Modeling And Verification Technology For Real-Time Embeded Software And Its Applications

The dependability requirements of Real-Time Embedded Systems(RTESs)are much higher than general-purpose software,because of their specificities in architecture,limited resource and working environment.The increasing complexity,scale and openness have brought great challenges to the development of dependable RTESs,and related researches have drawn great attention in recent years.Specifically,the analysis,verification and evaluation of the RTESs specifications at the early development stage can reduce potential flaws,thus lower the cost of testing and maintenance.This dissertation is aimed at exploring the basic theory and methodology of modeling,verifying and evaluating dependable RTESs,based on the formal semantics of Z notation.The effectiveness of the proposed methodology is validated through case studies on an implemented prototype.The main innovations of this dissertation can be summarized as follows:(1)An extensible model Z-MARTE for dependable RTESs is proposed,to provide rigorous semantics for the dependable structures and constraints.The time,structure and behavior aspects of RTESs are integrated in the Z-MARTE model,to extend the descriptive ability of Z towards dependable RTESs.The concept of dependability stereotype is introduced to specify generalized dependability constraints,including temporal and data constraints,which enable the rigorous and automated verification.(2)A verification method of Z-MARTE based on model checking technology is proposed.Firstly,based on the semantic interpretation of the Z-MARTE behavior with finite domain,a temporal logic is defined by extending CTL with a time duration operator,to describe the expected temporal properties of system behavior.And then,a symbolic model checking algorithm is proposed to verify the dependability constraints,which are expressed as temporal logic formulas.(3)A risk assessment method RAMES(Risk Assessment Method for Embedded Systems)complianced with ISO 31000 is proposed,to further evaluate and analyze the specification of RTESs.A formal model called OMR(Object-Message-Role)is derived from the Z-MARTE model,to integrate the functional and security aspects of RTESs,and to directly provide the input for risk assessment.An risk analysis algorithm is then proposed to perform the iterative risk calculation,and illustrated through a case study.(4)A prototype of the proposed modeling and verification methodology is established.A model transformation tool from MARTE to Z-MARTE is implemented on the Eclipse platform,to integrate their modeling environments.The key modules,including the parser of the Z-MARTE structure model,the generator of the Z-MARTE behavior model,and the model checker,are implemented on the VC 6.0 platform.A case study is given to illustrate the modeling and verification processes.