综合模块化航空电子系统安全分析的模型检测方法

A Model Checking Method for Safety Analysis of Integrated Modular Avionics System

综合模块化航空电子(IMA)系统可以在有效提高系统效率的同时减少资源的分配,但集成工作增加了系统的复杂性,同时使系统的故障在综合过程中传播到其他系统,这对系统的安全性也有很大的影响。传统的系统安全分析方法主要依赖于工程经验和个人技能,存在忽视系统故障状态和误判故障影响的局限性。为了解决该问题,提出了一种新的综合模块化航空电子系统安全分析方法——模型检测,使用遍历算法搜索所有系统状态。这种分析过程的使用在实现自动化的同时减少对工程经验的需求。该方法在综合模块化航空电子系统安全分析中的实用性得到验证,在系统需求规格的基础上给出了分析过程,利用模型检测工具NuSMV进行安全性分析。该方法能够自动识别出引起顶层事件的最小故障组合,从而达到传统故障树分析的目的,最终通过案例分析表明了该方法的实用性。

Integrated Modular Avionics(IMA) system can effectively improve the efficiency of the system and reduce the allocation of resources,but the integration work increases the complexity of the system,and causes the failure of the system to spread to other systems during the integration process,which has a great impact on the system security.Traditional system safety analysis methods mainly rely on engineering experience and personal skills,and have the limitation of ignoring system failure state and misjudging the impact of failure.In order to solve this problem,a new integrated modular avionics system safety analysis method called model checking is proposed,which uses the traversal algorithm to search all the system states.The use of this analysis process realizes automation and reduces the need for engineering experience.The practicability of this method in the safety analysis of integrated modular avionics system is verified.The analysis process is given based on the system requirements and specifications,and the model checking tool NuSMV is adopted for safety analysis.This method can automatically identify the minimum combination of faults that cause top-level events,so as to achieve the purpose of traditional fault tree analysis.Finally,the practicability of the method is demonstrated by the case analysis.