Research On Safety Modeling And Analysis Of EFVS Based On Model Checking

As a complex electronic system on the aircraft,the traditional safety analysis of enhanced flight vision system is faced with many problems,such as heavy workload,too much dependence on the experience of analysts,and easy to make mistakes.Although the formal methods such as Petri net and probability model improve the level of analysis automation and reduce a certain amount of analysis workload,they are also faced with the problem that safety requirements cannot be allocated from top to bottom.To solve these problems,a formal safety analysis method based on model checking is proposed.The qualitative and quantitative safety analysis of the enhanced flight scene system is realized to improve the analysis efficiency.The research includes the following aspects:(1)First of all,by abstracting the architecture and data flow of the system,which is divided into three levels: module level,LRU level and system level,the formal nominal model of the system is established and verified.(2)Study the method of model extension,write the fault database template,inject the fault mode of the underlying module into the nominal model,and establish the formal extension model.(3)The typical failure state is described by formal specification and calculated automatically to get the minimum cut set of fault tree.Based on the minimum cut set,qualitative and quantitative analysis is carried out.In the quantitative analysis,a safety allocation method is proposed and an automatic allocation tool is realized.The results show that the method is highly automatic,and solves the problem that other formal methods such as Petri nets and probability models can not carry out top-down probability allocation,which can more effectively promote the safety work in the system design stage.