计算机科学与探索2019，Vol.13Issue(8)：1295-1306,12.DOI:10.3778/j.issn.1673-9418.1806044
安全关键系统需求形式化建模分析实例研究*
Case Study of Formal Modeling Analysis for Safety-Critical System Requirements*
摘要
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.关键词
自动飞行控制系统(AFCS)/基于模型的安全性分析方法(MBSA)/NuSMV/xSAP/模型扩展/故障树/失效模式与影响分析(FMEA)表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分类
信息技术与安全科学引用本文复制引用
张维珺,胡军,李宛倩,陈朔,石梦烨,唐红英..安全关键系统需求形式化建模分析实例研究*[J].计算机科学与探索,2019,13(8):1295-1306,12.基金项目
The National Basic Research Program of China under Grant No. 2014CB744903 (国家重点基础研究发展计划(973计划)) （国家重点基础研究发展计划(973计划）
the Foun-dation of Graduate Innovation Center in Nanjing University of Aeronautics and Astronautics under Grant No. kfjj20171611 (南京航空航天大学研究生创新基地(实验室)开放基金) （南京航空航天大学研究生创新基地(实验室）
the Fundamental Research Funds for the Central Universities of China (中央高校基本科研业务费专项资金). （中央高校基本科研业务费专项资金）
