Abstract: In recent years, model-based safety analysis technology (MBSA) has been widely used in aviation and other fields. This study mainly discusses the safety evaluation method based on MBSA and the xSAP safety analysis platform. This method will be introduced in detail through an actual integrated avionics system Garmin G1000 automatic flight control system (AFCS) GFC700. The implementation of this method includes using NuSMV (new symbolic model verifier) formal language to model the system requirements, designing fault modes according to the system, injecting fault events into the NuSMV model, using the xSAP to extend the NuSMV requirement model to obtain the failure model and performing fault analysis and system safety evaluation on the failure model, such as generating a fault tree and a FMEA (failure mode and effect analysis) table. From the analysis results, it is effective to use the xSAP platform to perform model-based system safety analysis on actual systems.

Key words: automatic flight control system (AFCS), model-based safety analysis method (MBSA), new symbolic model verifier (NuSMV), extended safety assessment platform (xSAP), model extension, fault tree, failure mode and effect analysis (FMEA) table

摘要： 近年来，基于模型的安全性分析技术（MBSA）在航空等领域有着广泛应用，因此对以xSAP安全分析平台为核心，基于MBSA的系统安全性评估方法进行了研究，并通过一个真实的综合航电系统Garmin G1000的自动飞行控制系统（AFCS）GFC700为实例来详细介绍。该方法的实现包括使用NuSMV形式化语言对系统进行需求建模，根据系统设计故障模式，在NuSMV模型中注入故障事件，使用xSAP对NuSMV需求模型进行模型扩展得到故障扩展模型，以及对故障扩展模型进行故障分析及系统安全性评估，例如生成故障树及FMEA表等。从分析结果来看，使用xSAP平台对实际系统进行基于模型的系统安全分析是行之有效的。

关键词: 自动飞行控制系统（AFCS）, 基于模型的安全性分析方法（MBSA）, NuSMV, xSAP, 模型扩展, 故障树, 失效模式与影响分析（FMEA）表