安全关键系统需求形式化建模分析实例研究  

Case Study of Formal Modeling Analysis for Safety-Critical System Requirements

作　　者：张维珺 胡军[1] 李宛倩 陈朔 石梦烨 唐红英 ZHANG Weijun;HU Jun;LI Wanqian;CHEN Shuo;SHI Mengye;TANG Hongying(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院

出　　处：《计算机科学与探索》2019年第8期1295-1306,共12页Journal of Frontiers of Computer Science and Technology

基　　金：国家重点基础研究发展计划(973计划)No.2014CB744903;南京航空航天大学研究生创新基地(实验室)开放基金No.kfjj20171611;中央高校基本科研业务费专项资金~~

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]