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

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