在 HOL4 中集成 DFT 与 DRBD 的形式化
计算机科学中的逻辑
2019-10-22 v1
摘要
动态故障树（DFT）与动态可靠性框图（DRBD）是两种用于刻画工程系统动态失效行为以进行可靠性分析的建模方法。近来，在 HOL4 定理证明器中已开发了 DFT 与 DRBD 代数的两个独立的高阶逻辑（HOL）形式化。在本工作中，我们提出通过利用每种方法的优势来集成这两种建模方法，以实现复杂系统的高效形式化可靠性分析。该集成的可靠性由 DFT 与 DRBD 代数之间等价性的一份形式化证明所保证。我们以线控转向系统为例研究了所提出集成形式化可靠性分析的效率。
引用
@article{arxiv.1910.08875,
title = {Integrating DFT and DRBD Formalizations in HOL4},
author = {Yassmeen Elderhalli and Osman Hasan and Sofiene Tahar},
journal= {arXiv preprint arXiv:1910.08875},
year = {2019}
}