事件树的一个形式验证的HOL4代数
A Formally Verified HOL4 Algebra for Event Trees
摘要：
事件树（ET）分析作为一种前向演绎安全分析技术，在关键系统设计阶段被广泛用于决策。ET是表示系统中所有可能的操作状态和外部事件的示意图，以便这些可能的场景之一可能发生。在这份报告中，我们建议使用HOL 4定理证明的形式化建模和步骤分析的ET图。为此，我们在高阶逻辑中开发了一种基于通用列表数据类型的ET图的形式化，该数据类型可以：（i）构建任意级别的ET图;（ii）减少不相关的ET分支;（iii）划分ET路径;以及（iv）基于某些事件的发生进行概率分析。为了说明的目的，我们进行正式的ET逐步分析的电网，并确定其系统平均中断频率指数（SAIFI），这是一个重要的指标，系统的可靠性。
英文摘要：
Event Tree (ET) analysis is widely used as a forward deductive safety analysis technique for decision-making at the critical-system design stage. ET is a schematic diagram representing all possible operating states and external events in a system so that one of these possible scenarios can occur. In this report, we propose to use the HOL4 theorem prover for the formal modeling and step-analysis of ET diagrams. To this end, we developed a formalization of ETs in higher-order logic, which is based on a generic list datatype that can: (i) construct an arbitrary level of ET diagrams; (ii) reduce the irrelevant ET branches; (iii) partition ET paths; and (iv) perform the probabilistic analysis based on the occurrence of certain events. For illustration purposes, we conduct the formal ET stepwise analysis of an electrical power grid and also determine its System Average Interruption Frequency Index (SAIFI), which is an important indicator for system reliability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
