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

摘要：

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

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

所属期刊栏目：13

分类号：TP311(计算技术、计算机技术)

资助基金：The National Basic Research Program of China under Grant No. 2014CB744903 国家重点基础研究发展计划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

在线出版日期：2019-09-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：1295-1306