高阶逻辑中故障树的形式化：一种深度嵌入方法
计算机科学中的逻辑
2016-08-24 v1
摘要
故障树 (FT) 是一种标准的失效建模技术，已被广泛用于预测许多复杂工程系统的可靠性、可用性和安全性。为便于对基于 FT 的分析进行形式化分析，近期有人提出了 FT 的高阶逻辑形式化。然而，这种形式化在处理大型系统以及将 FT 模型转换为相应的可靠性框图 (RBD) 结构（即可靠性与可用性分析中一种常用的转换）方面相当受限。为克服这些局限，我们提出了一种基于深度嵌入的 FT 形式化方法。本文特别给出了 AND、OR 和 NOT FT 门的形式化，进而将其用于形式化其他常用 FT 门，即 NAND、NOR、XOR、Inhibit、Comparator 和多数 Voting 门，并对其失效概率表达式进行了形式验证。为便于说明，我们展示了针对下一代空中交通管理系统通信网关软件的形式化失效分析。
引用
@article{arxiv.1608.06392,
title = {Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach},
author = {Waqar Ahmed and Osman Hasan},
journal= {arXiv preprint arXiv:1608.06392},
year = {2016}
}
备注
arXiv admin note: text overlap with arXiv:1505.02648