基于模型检查的货运飞船推进剂在轨补加任务故障树分析方法研究

摘要：

针对货运飞船与空间实验室推进剂在轨补加任务过程,采用基于模型的安全性分析(Model Based Safety Analysis,MBSA)领域当下热门的建模语言SMV及其相应的形式化符号模型检查器NuSMV,对任务相关各系统进行故障树分析方法研究.通过模型检查过程自动快捷地验证预设的规范,分析反例序列和可达状态集,识别故障传播路径和最小割集,完成故障树定性分析.

关键词：故障树分析、模型检查、MBSA、NuSMV

分类号：TP311.56;V474;TP206.3

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

页数：共5页

页码：23-27