Research On Safety Analysis And Verification Methods For Embedded Systems Of Aerocraft

Embedded systems are widely applied into various safety critical fields such as aerospace and nuclear industries.For these systems(called Safety Critical Embedded Systems,SCESs),once a failure occurs,it will lead to serious property damage and even casualties.Therefore,safety analysis for SCESs has become more and more important.However,it becomes more and more difficult to analyze safety of embedded systems because of complexity,systematization and universality of systems.At present,there are some problems in embedded system safety analysis as follows: On the one hand,there is no overall safety analysis framework that cover embedded system layer to component layer;On the other hand,safety analysis methods mostly focus on system failure information,however,hardly consider static structure of system architecture.To address above problems,this thesis proposes a set of safety analysis methods for embedded systems of aircraft.The main contents are as follows:(1)For the issue of assignment for Functional Development Assurance Level(FDAL)in static architecture of system,FDAL-dependency-level-requirements are extracted from safety certification standards and used to check the consistency of the FDAL allocated in the actual system with safety certification standards.Firstly,the Sys ML block definition diagram(BDD)is extended to establish a safety design model for the static architecture of the system,and then the safety design model is transformed to a block dependency graph(BDG),which can accurately describe and verify the relationship on FDAL between the system components.Thirdly,we analyze the relevant safety standards and the influence of system architecture design on FDAL to capture the FDAL-dependency-level requirements.Finally,the consistency verification between the FDAL allocated in the system with extracted FDAL-dependency-level requirements is proposed based on BDG.(2)For the system safety risk analysis,a quantitative analysis method based on dynamic fault tree in two special scenarios is proposed.In this paper,a mapping method of dynamic fault tree model to temporal binary decision graph is proposed,and the minimum cut order set is obtained by traversing the ordered binary decision graph.In the case of mixed failure distribution,the probability calculation formula is obtained through the combination of failure paths,then the system failure probability is calculated.In the case of uncertainty distribution,we combined fuzzy theory and dynamic fault tree,then transformed the fuzzy dynamic fault tree into a fuzzy Markov chain model and calculate the fuzzy failure probability of the system.For the system failure behavior,the dynamic fault tree is used for modeling,and qualitative/quantitative safety analysis methods are proposed.The fuzzy theory is introduced to express the uncertainty in the embedded system.The minimum failure sequence leading to the danger and the fuzzy probability of occurrence of a hazard are obtained,which provides support for safety analysis and testing.(3)For the system failure states,a fault state reachability verification method based on fault state diagram is proposed.By extracting the safety requirement information from the system fault tree and describing it with BNF,the mapping table between safety requirements and state diagrams describes the transformation rules from fault tree logic gates and continuous time to state diagrams.The algorithm for constructing fault state diagrams automatically through fault tree and state diagram is designed.The semantic mapping between state diagram and time automata is established,then the fault state reachability is verified and analyzed by the model-checking tool UPPAAL.(4)Finally,based on the above methods,a tool for embedded system safety analysis tool(Tool4ESSA)is designed and implemented to support following analysis: safety analysis on the static structure,the minimum cut set analysis,failure probabilistic analysis,and reachability analysis on failure states.The effectiveness of these methods is illustrated by case study.