论文标题
事件树的正式验证的HOL4代数
A Formally Verified HOL4 Algebra for Event Trees
论文作者
论文摘要
事件树（ET）的分析被广泛用作在关键系统设计阶段进行决策的前额外包安全分析技术。 ET是一个示意图，代表系统中所有可能的操作状态和外部事件，因此可以发生这些可能的情况之一。在本报告中，我们建议将HOL4定理供款用于正式的建模和ET图的逐步分析。为此，我们在高阶逻辑中开发了ETS的形式化，该逻辑基于一个通用列表数据类型，该数据类型可以：（i）构造任意的ET图级别； （ii）减少无关的分支； （iii）分区和路径； （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.
