## On the Formalization of Importance Measures using HOL Theorem Proving
Waqar Ahmad 1 , Shahid Ali Murtza 2 , Osman Hasan 2 , and Sofiène Tahar 1
1 Electrical and Computer Engineering,
Concordia University, Montreal, QC, Canada
Email: {waqar,tahar}@ece.concordia.ca
2 School of Electrical Engineering and Computer Science,
National University of Sciences and Technology, Islamabad, Pakistan
Email: {smurtza.msee15seecs,osman.hasan}@seecs.nust.edu.pk
Abstract -Importance measures provide a systematic approach to scrutinize critical system components, which are extremely beneficial in making important decisions, such as prioritizing reliability improvement activities, identifying weak-links and effective usage of given resources. The importance measures are then in turn used to obtain a criticality value for each system component and to rank the components in descending manner. Simulations tools are generally used to perform importance measure based analysis, but they require expensive computations and thus they are not suitable for large systems. A more scalable approach is to utilize the importance measures to obtain all the necessary conditions by proving a generic relationship describing the relative importance between any pair of components in a system. In this paper, we propose to use higher-order-logic (HOL) theorem proving to verify such relationships and thus making sure that all the essential conditions are accompanied by the proven property. In particular, we formalize the commonly used importance measures, such as Birnbaum and Fussell-Vesely, and conduct a formal importance measure analysis of a railway signaling system at a Moroccan level crossing as an application for illustration purpose.
Keywords -Importance Measures, Higher-order Logic, Fault Tree, Theorem Proving.
## I. INTRODUCTION
Importance measures [1] provide an effective way to evaluate the relative criticality of components in a system. Particularly, they are employed to identify a subset of components that are more important to a system so that given resources can be effectively utilized. The underline concept is to focus on the most problematic areas in a system aiming to achieve the most significant gains. A study at Microsoft Corp. has revealed that about 20% of the entire pool of detected bugs lead to about 80% of the errors and crashes in Microsoft Windows and Office software [2]. In reliability engineering, determining the importance of components significantly helps to solve several reliability problems, such as component assignment, redundancy allocation, system upgrading, and fault diagnosis and maintenance.
In 1968, Birnbaum was the first to propose the concept of importance measure for binary systems of two states, either functioning or failed [3]. This led to the development of more sophisticated importance measures, such as FussellVesely [1], to analyze more complicated systems, like nuclear
The final publication is available at http://ieeexplore.ieee.org
power plants. These importance measures are primarily defined for coherent systems [1], which are systems satisfying the following conditions: (1) their structure function or system failure model exhibits non-decreasing behavior, i.e., the probability of the given failure model increases with the increase in the number of failures; and (2) each of their components is relevant, i.e., every component is actively contributing to the system failure.
A typical method in importance measure analysis involves calculating a criticality value for each component in a system and then tabulating the obtained data in descending manner [4]. In other words, a component with higher value is regarded as highly critical and placed above in the ranking than a component with a lower value. Simulation based reliability analysis tools, such as ReliaSoft [5], determine the component's importance by computing the percentage of times that a system failure event is caused by a failure of a particular component over the simulation time 0 to t . However, for analyzing the relative importance between all pairs of components, these methods have very high computational requirements especially when dealing with systems with many components.
The scalability limitations of simulation based importance measure analysis can be resolved by using mathematically verified reduction methods in this context. For instance, Boland et al. [6] developed a relationship stating that the component i is structurally more critical than the component j if its structure function is larger when i is down and j is up as compared to the opposite case. This work is further extended by Meng [7] to obtain the necessary conditions, based on Birnbaum and Fussell-Vesely importance measures, that are essential for proving the analytical relationships describing the relative importance of any pair of system components. These analytical relationships can be extremely helpful in practical scenarios since calculating the exact values of a component importance measures can be tedious for large and complex systems. However, these analytical relationships have been manually verified using paper-and-pencil based proof methods and thus there is no guaranty that all necessary conditions are explicitly identified. This is a grave concern considering the safety-critical nature of some importance measure analysis. Thus, there is a dire need of developing more rigorous analysis of these foundational relationships to guarantee their correctness and their appropriate usage.
In this paper, we propose to utilize higher-order-logic
(HOL) theorem proving to assure the formal guarantees about the relationships, obtained by Boland and Meng, governing the relative importance of any pair of system components. The HOL theorem prover is a system of deduction with precise semantics and provides a sound reasoning support for verifying the given properties, stated as a theorem, rigorously [8]. We first formalize the properties of coherent systems by describing their structure function as a fault tree (FT) [9] model, which is a graphical model for analyzing the conditions and factors causing the system failure. Secondly, we formalize commonly used importance measures, such as Birnbaum, Fussell-Vesely, Reduction Worth and Achievement Worth [1]. We then use the formalization of Birnbaum importance measure to formally verify the relative importance properties of any pair of system components as described by Boland and Meng using HOL theorem proving. For illustration purposes, we conduct the formal importance measure analysis of a railway signaling system at a Moroccan level crossing (LC) [10] consisting of several critical components, such as lights, programmable logic controllers, alarms and also human factor, using the HOL theorem prover [11].
The rest of the paper is organized as follows: An overview of the related work is presented in Section II. In Section III, we provide a brief summary of the HOL theorem prover and the fundamentals of the HOL probability theory. A brief introduction to the recent formalization of FT analysis is also described to facilitate the understanding of the paper. Section IV presents the HOL formalization of the concept of importance measure and its related properties. Section V applies our proposed approach by describing the formal importance measure analysis of the signaling system at a Moroccan level crossing. Finally, Section VI concludes the paper.
## II. RELATED WORK
Importance measure is a useful concept in reliability engineering and has been analyzed analytically [1] as well as using simulation tools [5]. The latter approach is practically adopted by industrial engineers due to their powerful features. These tools follow the typical approach of ranking the system components according to their criticality value. However, this approach requires high computations to obtain the criticality value for all system components and then perform the successive analysis, which may not be possible for large and complex systems. An alternate approach is to verify a relative measure relationship for any pair of components and obtain the necessary conditions, as described by Meng [7].
Recently, a formal dependability analysis framework [12], based on Reliability Block Diagram [13], [14] and FT modeling techniques, has been developed using HOL theorem proving. This framework has been successfully utilized to carry out the reliability analysis of a railway traction drive system [15], failure analysis of satellite solar arrays [16] and an air traffic management system [17]. In the current work, we formalize the notion of coherent system and the importance measure by representing the system structure function based on existing FT models. To the best of our knowledge, this is the first formal work describing the formalization of the importance measures using HOL theorem proving.
## III. PRELIMINARIES
In this section, we first give a brief introduction to the HOL theorem prover, formalization of probability theory and an approach for the formal FT analysis to facilitate the understanding of the rest of the paper.
## A. HOL Theorem Prover
HOL [18] is an interactive theorem prover, developed at the University of Cambridge, UK, for conducting proofs in higherorder logic. It utilizes the simple type theory of Church [19] along with Hindley-Milner polymorphism [20] to implement higher-order logic. HOL has been successfully used as a verification framework for both software and hardware as well as a platform for the formalization of pure mathematics.
The HOL core consists of only 4 basic axioms and 8 primitive inference rules, which are implemented as ML functions. The ML's type system ensures that only valid theorems can be constructed. Soundness is assured as every new theorem must be verified by applying these basic axioms and primitive inference rules or any other previously verified theorems/inference rules.
In this paper, we utilize the HOL theories (libraries) of Booleans, lists, sets, positive integers, real numbers, measure and probability [21]. In fact, one of the primary motivations of selecting the HOL theorem prover for our work was to benefit from these built-in mathematical theories. Table I provides the mathematical interpretations of some frequently used HOL symbols and functions, which are inherited from existing HOL theories.
TABLE I. HOL SYMBOLS AND FUNCTIONS
| HOL Symbol | Standard Symbol | Meaning |
|--------------|-------------------|---------------------------------|
| ∧ | and | Logical and |
| ∨ | or | Logical or |
| ¬ | not | Logical negation |
| :: | cons | Adds a new element to a list |
| ++ | append | Joins two lists together |
| HD L | head | Head element of list L |
| TL L | tail | Tail of list L |
| EL n L | element | n th element of list L |
| MEM a L | member | True if a is a member of list L |
| λ x . t | λx.t | Function that maps x to t ( x ) |
| SUC n | n +1 | Successor of a num |
## B. Probability Theory
Mathematically, a measure space is defined as a triple ( Ω , Σ , µ ), where Ω is a set, called the sample space, Σ represents a σ -algebra of subsets of Ω , where the subsets are usually referred to as measurable sets, and µ is a measure with domain Σ . A probability space is a measure space ( Ω , Σ , P r ), such that the measure, referred to as the probability and denoted by Pr , of the sample space is 1. In the HOL formalization of probability theory [21], given a probability space p , the functions space , subsets and prob return the corresponding Ω , Σ and Pr , respectively. This formalization also includes the formal verification of the commonly used probability laws, which play a pivotal role in formal reasoning about dependability properties.
A random variable is a measurable function between a probability space and a measurable space. The measurable functions belong to a special class of functions, which preserve the property that the inverse image of each measurable set is also measurable. A measurable space refers to a pair ( S, A ), where S denotes a set and A represents a nonempty collection of sub-sets of S . Now, if S is a set with finite elements, then the corresponding random variable is termed as a discrete otherwise it is called continuous.
The cumulative distribution function (CDF) is defined as the probability of an event where a random variable X has a value less than or equal to some value t , i.e., Pr ( X ≤ t ) . This definition characterizes the distribution of both discrete and continuous random variables and has been formalized [22]:
```
! \ \ p X t. CDF p X t =
distribution p X {y | y } \ Normal t)
```
The function Normal takes a real number as its input and converts it to its corresponding value in the extended -real data-type, i.e, it is the real data-type with the inclusion of positive and negative infinity. The function distribution takes three parameters: a probability space p , a random variable X : ( α → extreal ) and a set of extended -real numbers and returns the probability of the given random variable X acquiring all the values of the given set in probability space.
The unreliability or the probability of failure F ( t ) is defined as the probability that a system or component will fail by the time t . It can be described in terms of CDF, known as the failure distribution function, if a random variable X represents the time-to-failure of the component. This time-tofailure random variable X usually exhibits the exponential or Weibull distribution.
The notion of mutual independence of n random variables is a major requirement for reasoning about the failure analysis of the given systems. According to this notion, a list of n events are mutual independent if and only if for each set of k events, such that (1 ≤ k ≤ n ) , we have:
$$P r ( \bigcap _ { i = 1 } ^ { k } A _ { i } ) = \prod _ { i = 1 } ^ { k } P r ( A _ { i } ) \quad & ( 1 )$$
The mutual independence concept has been formalized in the HOL theorem prover and more details can be found in [22].
## C. Fault Trees
Fault Tree (FT) analysis is a widely used technique to determine the dependability of real-world systems, like railways signaling, automotive or avionics. It mainly provides a graphical model for analyzing the conditions and factors causing an undesired top event, i.e., a critical event, which can cause the complete system failure upon its occurrence. The preceding nodes of the FT are represented by gates, like OR, AND and XOR, which are used to link two or more cause events of a fault in a prescribed manner.
The FT gates are formally modeled by using a new recursive datatype gate in HOL as follows [17]:
```
serve
Hol_datatype 'gate = AND of gate list | OR of gate list | NOT of gate | atomic of 'a event'
```
The type constructors AND and OR recursively function on gate -typed lists and the type constructor NOT operates on gate -type variable. The type constructor atomic is basically a typecasting operator between event and gate -typed variables.
A semantic function is then defined over gate datatype that can yield the corresponding event from the given FT gate as follows:
```
[22]: follows:
! ( \a p. FTree p (AND []) = p_space p) ^
!( \a xs x p.
FTree p (AND (x::xs)) =
FTree p x \1 FTree p (AND xs)) ^
( \a p. FTree p (OR []) = {}) ^
( \a xs x p.
FTree p (OR (x::xs)) =
FTree p x U FTree p (OR xs)) ^
( \a p a.
FTree p (NOT a) =
p_space p DIFF FTree p a) ^
( \a p a. FTree p (atomic a) = a)
```
The function FTree takes a list of type gate , identified by the type constructor AND , and returns a complete probability space p\_space p if a given list is empty and otherwise returns the intersection of events in a given list. Similarly, to model the behavior of the OR FT gate, the function FTree returns the union of all the events after applying the function FTree on each element of a given list or an empty set if a given list is empty. The function FTree takes the type constructor NOT and returns the complement of a failure event obtained from the function FTree . The function FTree returns the failure event using the type constructor atomic .
If the occurrence of a failure event at the output is caused by the occurrence of all the input failure events, then this kind of behavior can be modeled by using the AND FT gate. Similarly, in the OR FT gate, the occurrence of an output failure event depends upon the occurrence of any one of its input failure event. The NOT FT gate can be used in conjunction with the AND and OR FT gates to formalize other FT gates. The formalization of these gates is based on [17], given in Table II. The NAND FT gate, represented by the function NAND\_FT\_gate in Table II, models the behavior of the occurrence of an output failure event when at least one of the failure events at its input does not occur. This type of gate is used in FTs when the non-occurrence of a failure event in conjunction with other failure events cause the top failure event to occur. This behavior can be expressed as the intersection of complementary and normal events, where the complementary events model the non-occurring failure events and the normal events model the occurring failure events. The output failure event occurs in the 2-input XOR FT gate if only one, and not both, of its input failure events occur.
The verification of the corresponding failure probability expressions, of the above-mentioned FT gates, is presented in Table III. These expressions are verified under the following assumptions: (i) prob\_space p ensures that p is
TABLE II. HOL FORMALIZATION OF FAULT TREE GATES
<details>
<summary>Image 1 Details</summary>
### Visual Description
## Table: Formalization of Logic Gates
### Overview
The image presents a table mapping five fundamental logic gates (AND, OR, NAND, NOR, XOR) to their formalized representations using logical operators and a function called `FTTree`. Each gate is depicted with its standard symbol and annotated with variables (e.g., `n`, `-1`, `-k`), while the corresponding formalization uses logical expressions and nested function calls.
---
### Components/Axes
- **Columns**:
1. **FT Gates**: Contains symbols for logic gates with annotations.
2. **Formalization**: Contains logical expressions using `FTTree`, `AND`, `OR`, `NOT`, and `gate_list`.
- **Annotations**:
- **AND Gate**: Labeled with `n` (input count).
- **NAND Gate**: Annotated with `-1` (inversion) and `-k` (complement).
- **NOR Gate**: Annotated with `-1` (inversion) and `-n` (negated input count).
- **XOR Gate**: Annotated with `-2` (two inputs).
---
### Detailed Analysis
#### Row 1: AND Gate
- **Symbol**: Standard AND gate with `n` inputs.
- **Formalization**:
`AND_FT_gate p L1 L2 = FTree p (AND (gate_list L))`
*Interpretation*: Represents an AND gate with inputs `L1` and `L2`, formalized using `FTTree` and `gate_list`.
#### Row 2: OR Gate
- **Symbol**: Standard OR gate with `n` inputs.
- **Formalization**:
`OR_FT_gate p L = FTree p (OR (gate_list L))`
*Interpretation*: Represents an OR gate with inputs `L`, formalized using `FTTree` and `gate_list`.
#### Row 3: NAND Gate
- **Symbol**: NAND gate with `-1` (inversion) and `-k` (complement) annotations.
- **Formalization**:
`NAND_FT_gate p L1 L2 = FTree p (AND (gate_list(compl_list p L1 ++ L2)))`
*Interpretation*: Combines `L1` (complemented) and `L2` via `compl_list`, then applies `AND` and `FTTree`.
#### Row 4: NOR Gate
- **Symbol**: NOR gate with `-1` (inversion) and `-n` (negated input count) annotations.
- **Formalization**:
`NOR_FT_gate p L = FTree p (NOT (OR (gate_list L)))`
*Interpretation*: Applies `NOT` to the result of `OR` over `gate_list L`, then uses `FTTree`.
#### Row 5: XOR Gate
- **Symbol**: XOR gate with `-2` (two inputs) annotation.
- **Formalization**:
`XOR_FT_gate p A B = FTree p (OR [AND [NOT A; B]; AND [A; NOT B]])`
*Interpretation*: Implements XOR as `(A AND NOT B) OR (NOT A AND B)` using nested `AND`/`NOT` operations.
---
### Key Observations
1. **Consistency**: All formalizations use `FTTree` as a wrapper function, suggesting a unified framework for gate representation.
2. **Complement Handling**: NAND and NOR gates explicitly use `compl_list` and `NOT` to handle inverted inputs.
3. **XOR Complexity**: XOR is decomposed into a combination of `AND`, `NOT`, and `OR`, reflecting its non-linear nature.
---
### Interpretation
This table formalizes logic gates into a structured format likely for use in formal verification, hardware description languages (HDLs), or symbolic computation. The `FTTree` function appears central, possibly representing a tree-based abstraction for gate operations. The annotations (`n`, `-1`, `-k`) indicate input counts and inversion rules, critical for defining gate behavior in formal systems. The decomposition of XOR into basic operations highlights the table’s focus on breaking down complex logic into foundational components.
</details>
| FT Gates | Formalization |
|------------|---------------------------------------------------------------------------------------------------|
| AND 1 n | /turnstileleft ∀ p L1 L2. AND_FT_gate p L1 L2 = FTree p (AND (gate_list L)) |
| OR 1 n | /turnstileleft ∀ p L. OR_FT_gate p L = FTree p (OR (gate_list L)) |
| NAND 1 n k | /turnstileleft ∀ p L1 L2. NAND_FT_gate p L1 L2 = FTree p (AND (gate_list(compl_list p L1 ++ L2))) |
| N OR 1 n | /turnstileleft ∀ p L. NOR_FT_gate p L = FTree p (NOT (OR (gate_list L))) |
| XOR 1 2 | /turnstileleft ∀ p A B. XOR_FT_gate p A B = FTree p (OR [AND [NOT A; B]; AND [A; NOT B]]) |
a valid probability space; (ii) 2 ≤ LENGTH L makes sure that the given list L must have at least two elements; (iii) in\_events p L ensures that all the corresponding events in the given list L are drawn from the events space p ; and (iv) mutual\_indep p L guarantees that events in the given list L are mutually independent [22].
TABLE III. PROBABILITY OF FAILURES OF FAULT TREE GATES
<details>
<summary>Image 2 Details</summary>
### Visual Description
## Table: Mathematical Expressions and Theorem Conclusions
### Overview
The image presents a structured table with two columns: "Mathematical Expressions" and "Theorem's Conclusion". Each row pairs a probabilistic/mathematical definition with a corresponding logical conclusion involving propositional logic (P), list operations, and gate functions (e.g., AND_FT_gate, OR_FT_gate). The table appears to formalize relationships between probabilistic events and logical operations.
### Components/Axes
- **Columns**:
1. **Mathematical Expressions**: Contains probabilistic definitions (e.g., intersections, unions, products) and recursive formulas.
2. **Theorem's Conclusion**: Contains logical equivalences (⊨) and mappings to propositional logic (P), list operations (list_prod, list_prod_one_minus_list), and gate functions (AND_FT_gate, OR_FT_gate).
### Detailed Analysis
#### Row 1
- **Mathematical Expression**:
```
F_AND(t) = Pr(∩_{i=2}^N A_i(t)) = ∏_{i=2}^N F_i(t)
```
- **Theorem's Conclusion**:
```
⊨ ∨ p P L L2. (prob p (AND_FT_gate p L) = (list_prod (list_prod p L))
```
- **Interpretation**: The probability of the intersection of events `A_i(t)` equals the product of individual probabilities `F_i(t)`. This maps to a logical conclusion where the AND_FT_gate operation on `p` and `L` corresponds to nested list products.
#### Row 2
- **Mathematical Expression**:
```
F_OR(t) = Pr(∪_{i=2}^N A_i(t)) = 1 - ∏_{i=2}^N (1 - F_i(t))
```
- **Theorem's Conclusion**:
```
⊨ ∨ p P L L2. (prob p (OR_FT_gate p L) = (list_prod (list_prod (1 - list_prod (one_minus_list p)) L))
```
- **Interpretation**: The probability of the union of events is derived via inclusion-exclusion. The OR_FT_gate maps to a nested list product involving the complement of `p` and `L`.
#### Row 3
- **Mathematical Expression**:
```
F_NAND(t) = Pr(∩_{i=2}^k Ā_i(t) ∩ ∩_{j=k+1}^N A_j(t)) = ∏_{i=2}^k (1 - F_i(t)) * ∏_{j=k+1}^N F_j(t)
```
- **Theorem's Conclusion**:
```
⊨ ∨ p P L L2. (prob p (NAND_FT_gate p L L2) = (list_prod (list_prod p L) * (list_prod (list_prod (compl_list p L1)) L2))
```
- **Interpretation**: The NAND_FT_gate combines two list products: one for `p` and `L`, and another for the complement of `p` (L1) and `L2`.
#### Row 4
- **Mathematical Expression**:
```
F_NOR(t) = 1 - F_OR(t) = ∏_{i=2}^N (1 - F_i(t))
```
- **Theorem's Conclusion**:
```
⊨ ∨ p P. (prob p (NOR_FT_gate p L) = (list_prod (one_minus_list (list_prod p L)))
```
- **Interpretation**: The NOR_FT_gate inverts the list product of `p` and `L`, reflecting the negation of the OR operation.
#### Row 5
- **Mathematical Expression**:
```
F_XOR(t) = Pr((Ā(t) ∩ B(t)) ∪ (A(t) ∩ B̄(t))) = (1 - F_A(t))F_B(t) + F_A(t)(1 - F_B(t))
```
- **Theorem's Conclusion**:
```
⊨ ∨ p P A B. (prob p (XOR_FT_gate p A B) = (1 - prob p A) * prob p B + prob p A * (1 - prob p B))
```
- **Interpretation**: The XOR_FT_gate maps to a probabilistic combination of `A` and `B` events, mirroring the XOR formula.
### Key Observations
1. **Recursive Structure**: Many expressions (e.g., F_AND, F_OR) use recursive products over indices, suggesting hierarchical event dependencies.
2. **Logical-Gate Mapping**: Each probabilistic function (AND, OR, NAND, NOR, XOR) corresponds to a specific gate operation with list-based interpretations.
3. **Complement Operations**: Terms like `one_minus_list` and `compl_list` indicate explicit handling of event negations in logical conclusions.
4. **List Product Recursion**: Nested list products (e.g., `list_prod (list_prod p L)`) imply multi-stage aggregation of probabilistic outcomes.
### Interpretation
The table formalizes a framework where probabilistic events (modeled as intersections/unions of `A_i(t)`) are translated into propositional logic via gate functions. These gates (AND_FT_gate, OR_FT_gate, etc.) operate on lists (`L`, `L1`, `L2`) using list products and complements, bridging probability theory and formal logic. This structure likely supports theorem proving or formal verification systems, where probabilistic outcomes are decomposed into logical operations for analysis or automation. The recursive and nested nature of the expressions suggests scalability to complex event interactions.
</details>
| Mathematical Expressions | Theorem's Conclusion |
|-------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------|
| F AND ( t ) = Pr ( N ⋂ i =2 A i ( t )) = N ∏ F i ( t ) | /turnstileleft ∀ p L1 L2. (prob p (AND_FT_gate L) = list_prod (list_prob p L)) |
| i =2 F OR ( t ) = Pr ( N ⋃ i =2 A i ( t )) = 1 - N ∏ i =2 (1 - F i ( t )) | /turnstileleft ∀ p L1 L2. (prob p (OR_FT_gate p L) = 1 - list_prod(one_minus_list (list_prob p L))) |
| F NAND ( t ) = Pr ( k ⋂ i =2 A i ( t ) ∩ N ⋂ j = k A i ( t )) = k ∏ i =2 (1 - F i ( t )) ∗ N ∏ j = k ( F j ( t )) | /turnstileleft ∀ p L1 L2. (prob p (NAND_FT_gate p L1 L2) = list_prod (list_prob p (compl_list p L1)) * list_prod (list_prob p L2)) |
| F NOR ( t ) = 1 - F OR ( t ) = N ∏ i =2 (1 - F i ( t )) | /turnstileleft ∀ p L. (prob p (NOR_FT_gate p L) = list_prod (one_minus_list (list_prob p L))) |
| F XOR ( t ) = Pr ( A ( t ) B ( t ) ∪ A ( t ) B ( t )) = (1 - F A ( t )) F B ( t )+ F A ( t )(1 - F B ( t )) | /turnstileleft ∀ p A B. prob_space p ∧ A ∈ events p ∧ B ∈ events p ⇒ (prob p (XOR_FT_gate p A B) = (1 - prob p A) * prob p B + prob p A * (1 - prob p B)) |
## D. PIE Principle
In FT analysis, the first step is to identify all the basic failure events that can cause the occurrence of the system top failure event. These failure events are then combined to model the overall fault behavior of a given system by using the fault gates. These combinations of basic failure events, called cut sets, are then reduced to minimal cut sets (MCS) by using set-theory rules, such as idempotent, associative and commutative. Then, the Probabilistic Inclusion Exclusion (PIE) principle is used to evaluate the overall failure probability of a given system based on the MCS events. According to the PIE principle, if A i represents the i th basic failure event or a combination of failure events, then the overall failure probability of a given system can be expressed as follows:
$$\mathbb { P } ( \bigcup _ { i = 1 } ^ { n } A _ { i } ) = \sum _ { t \neq \{ \} , t \subseteq \{ 1 , 2 , \dots , n \} } ( - 1 ) ^ { | t | + 1 } \mathbb { P } ( \bigcap _ { j \in t } A _ { j } ) \quad ( 2 )$$
/negationslash
The above equation has been formally verified in HOL and details can be found in [17].
## IV. IMPORTANCE MEASURES
The concept of importance measure is proposed by Birnbaum mainly for components of coherent systems. This section describes the essential properties of a coherent system that is then followed by the commonly used importance measures and their respective formalizations in HOL.
## A. Coherent System
Let, φ (¯ x ) be the structure function of a system functioning on the n -components state vector ¯ x = ( x 1 , x 2 , . . . , x i , . . . , x n ) , where x i is the state of the i th component. According to Birnbaum [3], a system of binary state, where both the system and its components can either be in state of failure or success, is said to be coherent if its structure function, φ (¯ x ) , satisfies the following conditions:
- (1) φ ( ¯ 0) = 0 with ¯ 0 = (0 , 0 , . . . , 0)
$$( 2 ) \quad \phi ( \bar { 1 } ) = 1 w i t h \bar { 1 } = ( 1 , 1 , \dots , 1 )$$
$$\begin{array} { r l } & { ( 3 ) \quad \phi ( \bar { x } ) \leq \phi ( \bar { y } ) i f \bar { x } \leq \bar { y } w i t h r e l a t i o n s h i p \bar { x } \leq \bar { y } m e a n s } \\ & { \quad x _ { i } \leq y _ { i } , \forall i = 1 , 2 , \dots n . } \end{array}$$
The first two conditions state that a system must go in state 0 (full working) or 1 (complete failure) if all of its components are in state 0 or 1, respectively. The third condition defines the monotonicity property of a system structure function ensuring that a component in working state must not contribute in causing a system failure and vice versa. The use of the NOT gate in a FT model (structure function) results in a noncoherent structure, which also means that components not failing, i.e., working, can contribute to a system failure event and thus violating the condition (3). Therefore, the use of the NOT logic is often discouraged [23].
In order to formally verify that a given failure structure function (FT model) satisfies the Birnbaum coherent system conditions, we first formally define a structure function in HOL as follows:
## Definition 1: /turnstileleft ∀ f L. φ f L = f L
where φ is a HOL Unicode character that is used as a prettyprinting of the function coherent\_struct mapping an arbitrary real-valued function f : ( α → bool ) → real to a list of sets L : ( α → bool ) list . Using the above definition, Conditions (1-2) can be verified in HOL on a given fault tree (structure function) consisting of AND and OR FT gates as:
```
event
failure
ws:
coherent_state_vec (a. a = {}) (FLAT L) =>
```
```
(prob p
(phi (lambda.
FTree p ((OR of
(lambda. AND (gate list a))) b)) L) = 0)
```
where, the HOL function FLAT is used to flatten the twodimensional list, i.e., to transform a list of lists, into a single list. The assumptions in the above theorems are almost similar. The first two assumptions ensure that the variable p is a valid probability space and the given list of state vectors is not empty. In the last assumption, the function coherent\_state\_vec asserts that all the system components are either in fully working or in completely failure state, which are modeled using empty event ({}) and the complete probability space ( p\_space p ), respectively. The conclusions of the above theorems model the probabilistic sense of the conditions (1-2).
Now, we formally verify the Condition 3 for the given structure function in HOL as follows:
```
structure function in HOL as follows:
Theorem 3: |- \p L.
prob_space p /\
in_events p (FLAT (XL_vec L)) /\
in_events p (FLAT (YL_vec L)) /\
mem_subset_vec L =>
prob p
( \phi ( \b.
FTree p((OR of
(Aa. AND (gate_list a))) b)) (XL_vec L)) \
prob p
( \phi ( \b.
FTree p ((OR of
(Aa. AND (gate_list a))) b)) (YL_vec L))
```
where the function in\_events ensures that each element of a given list belongs to a valid event space p . The functions XL\_vec and YL\_vec returns the first and second member of the two-dimensional pair list, respectively. The relationship between these two lists, XL\_vec and YL\_vec , is described by the function mem\_subset\_vec , which ensures that each member of XL\_vec list is a subset of the corresponding member of YL\_vec list. The conclusion of the above theorem models Condition 3. The proof of Theorem 3 follows from the fact that if A ⊆ B , then their corresponding probabilities satisfy the monotonicity property, i.e., Pr( A ) ≤ Pr( B ) .
## B. Birnbaum Importance
For a coherent system of n -components with independent failures, the Birnbaum importance ( I ( i ) B ) of component i is defined as a probability that the i th component is critical to the system failure or functioning. Mathematically, it can be expressed as follows [3]:
$$\frac { \partial h ( \bar { x } ) } { \partial p _ { i } } = I ^ { ( i ) } _ { B } ( \phi ( \bar { x } ) ) = P r \{ \phi ( ( 1 _ { i } , \bar { x } ) ) \} - P r \{ \phi ( ( 0 _ { i } , \bar { x } ) ) \}$$
where φ (¯ x ) represents the structure function of a given coherent system, which is applied on components state vector ¯ x and returns the corresponding state of a system. The notations φ ((1 i , ¯ x )) and φ ((0 i , ¯ x )) represent the state of a system if the i th component is updated with the state values 1 (failure) and 0 (working), respectively.
To formalize Equation 3 in HOL, we first formally define the notion of component state update in a given structure function as follows:
```
<loc_0><loc_1><loc_500><loc_500><_FORTRAN_>Definition 2: - \forall i f L.
phi' e i f L = phi f (LUPDATE ei l)
```
where the HOL function LUPDATE updates the given list L with element e at index i . The above function updates the state of the component i in a state vector L before passing it to the system structure function. Similarly, we can formally define a function to update the states of any two system components in HOL as follows:
```
Definition 3: !e' e' i j f L.
!e' f (LUPDATE e' j (LUPDATE e i L))
```
Now, using Definition 2, we can formally model Equation 3 in HOL as follows:
```
Definition 4: I$_{β}$ p i f L =
prob p (φ' (p_space p) i f L) -
prob p (φ' {} i f L)
```
As described earlier in Section I, Meng [7] developed the analytical relationship describing the relative importance of any pair of system components and obtained the necessary conditions based on Boland and Birnbaum importance measures. We formally verify this relationship in HOL as follows:
Theorem 4: Meng [7]: Suppose that i c = j and ∂ 2 h ( x ) ∂p i ∂p j ≥ 0 for all x . Then, I β (j, x ) ≤ I β (i, x ) for all x satisfying p i ≤ p j .
```
#shipin
#scribed
[A1]: prob_space p ^ in_events p L ^
[A2]: ~NULL L ^ i < j ^
[A3]: mutual_indep p
[{} :: {} ::p_space p::p_space p::L) ^
[A4]: SUC (SUC j) < LENTH L ^
[A5]: I'^ b p i j
(lambda. FTree p (AND (gate_list a))) L > 0 ^
[A6]: prob p (EL i L) \< prob p (EL j L) =>
(I_b p j (a. FTree p (AND (gate_list a)))) L \leq
I_b p i (a. FTree p (AND (gate_list a))) L)
```
In the above statement, the symbol i c = j is described by Boland et al. [6] as components i and j are permutation equivalent if φ (1 i , 0 j , x ) = φ (0 i , 1 j , x ) for all x . Using Definition 3, we formally verify this property in HOL as follows:
$$\begin{array} { r l } { L e m m a 1 \colon \, \vdash \, \forall \, p \, i \, j \, L . \, p r o b _ { s p a c e } p \, \wedge \, i < j \, \wedge } \\ { i n _ { - } e v e n t s \, p \, L \, \wedge \, S U C \, ( S U C \, j ) < \, L E N G T H \, L \, \wedge } \\ { m u t u a l _ { - } i n d e p \, p \, ( \{ \} \, \colon p _ { - } s p a c e \, p \, \L L ) \Rightarrow } \\ { ( p o b \, p \, ( \phi ^ { \prime } \, ( p _ { - } s p a c e \, p ) \, \{ \} \, i \, j ) \, ( \lambda a . \, F T r e e \, p \, ( A N D \, ( g a t e _ { - } l i s t \, a ) ) \, L ) = } \\ { p o b \, p \, ( \phi ^ { \prime } \, ( p _ { - } s p a c e \, p ) \, i \, j ) } \\ { ( \lambda a . \, F T r e e \, p \, ( A N D \, ( g a t e _ { - } l i s t \, a ) ) \, L ) ) } \end{array}$$
Similarly, the notation ∂ 2 h ( x ) ∂p i ∂p j is a partial differentiation w.r.t probability of components i and j that can be represented mathematically as:
$$\frac { \partial ^ { 2 } h ( x ) } { \partial p _ { i } \partial p _ { j } } = & \Pr ( \phi ^ { ^ { \prime \prime } } ( 1 _ { i } , 1 _ { j } , \mathbf x ) ) - \Pr ( \phi ^ { ^ { \prime } } ( 1 _ { i } , 0 _ { j } , \mathbf x ) ) - & ( 4 )$$
The above equation is formalized using Definition 3 and it is represented by the function I ′′ β in the assumption (A5) of Theorem 4.
The assumptions of Theorem 4 are similar to the ones used in Theorems 1-3. The inclusion of {} and p\_space p in assumption (A3) reflects the change caused by flipping the state of the i and j components and also makes sure that they are mutually independence. The assumption (A4) ensures that the index j starts after two increments since we require at least two components in a list. Although a brief proof sketch of Theorem 4 is described by Meng [7], the sound environment of the HOL theorem prover provides additional formal guarantees in the verification of Theorem 4 accompanying all the necessary conditions. The formal proof of Theorem 4 utilizes several essential lemmas, which can be found in [24].
## C. Other Common Types of Importance Measures
Another well-known importance measure is FussellVesely [1], which describes the importance of component i as a probability that the failure of component i contributes to a system failure given that system fails. It can be expressed mathematically as follows:
$$I _ { F V } = \frac { P r ( \phi ( x ) ) - P r ( \phi ^ { \prime } ( 1 _ { i } , x ) ) } { P r ( \phi ( x ) ) }$$
We can formally define the above function by using Definitions 1-2 in HOL as follows:
$$\begin{array} { r l } { \text {Definition 5.} \vdash \forall f i L . } \\ { I _ { F V } p i f L = } \\ { \frac { p r o b p ( \phi f L ) - p r o b p ( \phi ^ { \prime } ( p _ { S p a c e } p ) i f L ) } { p r o b p ( \phi f L ) } } \end{array}$$
Similarly, the criticality importance measures Reducation Worth ( I RW ) and Achievement Worth ( I AW ) describe a probability when component i is always functioning and failed, respectively. They can be expressed as follows:
$$\begin{array} { r l } & { I _ { R W } = \frac { P r ( \phi ( x ) ) } { P r ( \phi ^ { \prime } ( 1 _ { i } , x ) ) } } \\ & { I _ { A W } = \frac { P r ( \phi ^ { \prime } ( 0 _ { i } , x ) ) } { P r ( \phi ( x ) ) } } \end{array} ( 6 )$$
Using Definitions 1-2, we formally define the above functions in HOL as follows:
<!-- formula-not-decoded -->
The HOL formalization of the above-mentioned importance measures is also available at [24]. The proof script of the above formalizations and proofs consists of about 1400 lines of HOL code that roughly took 70 man-hours of development time. To illustrate the effectiveness of our proposed approach, we conduct the formal importance measure analysis of a railway signaling system at Moroccan level crossing in the next section.
## V. SIGNALING SYSTEM AT MOROCCAN LEVEL CROSSING
There are three main parts in the Moroccan level crossing railway signaling (LC) system [10]: (1) Rail part consisting of a material component (train and rail-road), and human component (the train operator); (2) Road part containing a material component (vehicle and road), and a human component (vehicle driver); and (3) Level crossing, which is further composed of three main components: (i) Power and communication network between the components of the railway signaling system; (ii) Control component consisting of Programmable Logic Controller and its program; (iii) Operative component representing sensors, such as road lights, the alarms and the barriers. Table IV describes the basic failure events along with the corresponding failure rates ( λ ) associated with the components of Moroccan signaling system [10]. The FT diagram of the signaling system at Moroccan LC is depicted in Figure 1 [10].
TABLE IV. EVENTS FOR SIGNALING SYSTEM AT MOROCCAN LC
| Symbol | Basic Events | λ ( h - 1 ) |
|-----------|---------------------------------------|------------------|
| x1 | Vehicle Failure | 18 ∗ 10 - 3 |
| x2 & x4 | Human Factor | 1 . 347 ∗ 10 - 4 |
| x3 | Rail Failure | 2 . 85 ∗ 10 - 6 |
| x5 | Program Error | 5 ∗ 10 - 8 |
| x6 | Programmable Logic Controller Failure | 4 ∗ 10 - 6 |
| x7 | Network Communication Failure | 5 ∗ 10 - 6 |
| x8 | Power Network Failure | 5 ∗ 10 - 6 |
| x9 & x10 | Alarm Failure | 4 ∗ 10 - 4 |
| x11 & x12 | Light Failure | 4 ∗ 10 - 4 |
| x13 & x14 | Motor Failure | 3 ∗ 10 - 6 |
| x15 & x16 | Transmission System Failure | 5 ∗ 10 - 5 |
## A. Formal Model and Failure Analysis
Using the FT gates, described in Section III-C, we can formally model the FT diagram of the Moroccan signaling system in HOL as follows:
<details>
<summary>Image 3 Details</summary>
### Visual Description
## Hierarchical Diagram: Top Event Structure
### Overview
The image depicts a hierarchical tree diagram with a central "Top Event" node at the apex, branching into multiple levels of sub-nodes. Each node is labeled with a unique identifier (e.g., x1, x2, ..., x16), and the structure follows a branching pattern where each parent node splits into two or three child nodes. The diagram emphasizes hierarchical relationships and connectivity between nodes.
### Components/Axes
- **Top Event**: The root node at the top of the diagram, serving as the origin of all branches.
- **Nodes**: Labeled x1 to x16, arranged in a tree-like structure. Each node is connected to its parent via a vertical line, with child nodes positioned directly below.
- **Branching Pattern**:
- The "Top Event" splits into three primary branches:
1. Left branch (x3, x4)
2. Middle branch (x5, x6)
3. Right branch (x1, x2)
- The middle branch (x5, x6) further splits into two sub-branches: x8 and x7.
- Subsequent levels show additional splits, culminating in the bottom level with x13, x14, x15, and x16.
### Detailed Analysis
- **Labels and Positions**:
- **Top Event**: Centered at the top, connected to three primary branches.
- **First-Level Nodes**:
- Left: x3 (left) and x4 (right) under the left branch.
- Middle: x5 (left) and x6 (right) under the middle branch.
- Right: x1 (left) and x2 (right) under the right branch.
- **Second-Level Nodes**:
- Middle branch splits into x8 (left) and x7 (right).
- **Third-Level Nodes**:
- x8 splits into x9 (left) and x10 (right).
- x7 splits into x11 (left) and x12 (right).
- **Bottom-Level Nodes**:
- x9 splits into x13 (left) and x14 (right).
- x10 splits into x15 (left) and x16 (right).
- x11 and x12 do not have further splits in the diagram.
- **Flow Direction**: All connections flow downward from parent to child nodes, with no upward or lateral connections.
### Key Observations
- The diagram is strictly hierarchical, with no cycles or feedback loops.
- The labeling follows a sequential pattern (x1 to x16), but the distribution is uneven across branches.
- The middle branch (x5, x6) has the most complex sub-structure, with two additional splits (x8, x7) and their children.
- The bottom level (x13–x16) represents the terminal nodes with no further branching.
### Interpretation
This diagram likely represents a process flow, decision tree, or organizational structure where each node signifies a discrete event, decision, or component. The "Top Event" acts as the initiating point, with subsequent nodes representing sub-events or dependencies. The uneven branching suggests variability in the complexity or number of sub-events at different stages. The absence of feedback loops implies a linear progression from the top event to terminal nodes. The labels (x1–x16) may correspond to specific stages, tasks, or entities in a larger system, though their exact meaning is not provided in the image.
</details>
Fig. 1. FT of the Signaling System at Moroccan LC
```
Definition 8: |- Signal_FT p x1 x2 ... x16 t =
FTree p (OR [OR ([w p x3 t;w p x4 t])
OR ([w p x5 t;w p x6 t]));
AND [OR ([w p x9 t;w p x10 t]));
OR ([w p x13 t;w p x14 t]));
OR ([w p x15 t;w p x16 t]));
OR ([w p x11 t;w p x12 t]))];
OR ([w p x7 t;w p x8 t]));
OR ([w p x1 t;w p x2 t]))])
```
where ω p x t represent various failure events, such as an alarm, associated with the various component of the Moroccan signaling system. It is defined in HOL as PREIMAGE x {y | y ≤ t} ∩ p\_space p [17].
Now, we obtain the minimal cut sets (MCS) of the above FT model by utilizing some set properties, like distribution of intersection over union and idempotent law of intersection [9].
$$C _ { 1 } = \{ x 3 , x 4 , x 5 , x 6 \} , C _ { 2 } = \{ x 9 , x 1 3 , x 1 5 , x 1 1 \} , \cdots , \quad ( 7 )$$
We can also formally verify the equivalence of the obtained signaling system MCS with the orignal FT model as follows:
```
Lemma 2: |- Signal_FT p x1 x2 ·· x16 t =
(λb.
FTree p((OR of
(λa. AND (gate_list a))) b))
[ωL p [x3;x4;x5;x6] t;
ωL p [x9;x13;x15;x11] t;···;
ωL p [x10;x14;x16;x12] t;
ωL p [x7;x8;x1;x2] t]
```
where the function ω L p L t returns the list of events by mapping the function ω p x t , described in Definition 8, on each element of the given list of random variables.
By using the above lemma and Definition 8, the failure probability of the Moroccan signaling system can be formally verified in HOL as follows:
```
Theorem 6: |- \p x1 x2 ... x16 c1 c2 ... c16 t.
[A1]: 0 < t ^
[A2]: FT_conds p [x1;x2;...;x16] t
[A3]: exp_dist_list p [x1;x2;...;x16]
[c1;c2;...;c16] =>
(prob p (Signal_FT p x1 x2 ... x16 t) =
1 - e-(\c3t) * e-(-(\c4t) * e-(-(\c5t) * e-(-(\c6t) * e-(-(\c7t) * e-(-(\c8t) * e-(-(\c9t) * e-(-(\c10 t)) * e-(-(\c11 t)) *)
(1 - (1 - e-(\c13 t) * e-(-(\c14 t)) * e-(-(\c15 t) * e-(-(\c16 t)) * e-(-(\c17 t) * e-(-(\c18 t)) * e-(-(\c19 t)) *)
(1 - e-(\c15 t) * e-(-(\c16 t)) * e-(-(\c11 t) * e-(-(\c12 t)) * e-(-(\c13 t) * e-(-(\c14 t) * e-(-(\c15 t) * e-(-(\c16 t) * e-(-(\c17 t) * e-(-(\c18 t) * e-(-(\c19 t)))) *)
```
where the function exp\_dist\_list takes a list of random variables and a list of failure rates and makes sure that each random variable is exponentially distributed and assigned with its corresponding failure rates [17], i.e., exp\_dist\_list [x1;x2] [c1;c2] = (!t. 0 ≤ t ==> (( Pr( ω p x 1 t ) = 1 -e -λ c 1 ∗ t ) ∧ ( Pr( ω p x 2 t ) = 1 -e -λ c 2 ∗ t )) . The function FT\_conds contains two predicates mutual\_indep and in\_events , which ensure that all events associated to rail\_signal\_FT are mutually independent and belong to events space p , respectively. The proof of Theorem 6 is based on formally verified expressions of the AND and OR FT gates, presented in Table III, and the PIE principle described in Section III-D.
To evaluate Theorem 6, we wrote an ML function auto\_signal\_morco\_FT [24] that takes failure rates and time index, given in Table IV, and returns the following in HOL evironment:
## Under the following assumptions
```
roccan
x {y
[A2]: FT_conds p [x1;x2;...;x16] 5
[A3]: exp_dist_list p [x1;x2;...;x16]
[0.00000285;0.00000005;...;0.0004] =>
```
## Failure probability of Moroccan Railway Signaling System
(prob p (Signal\_FT p x1 x2 · · · x16 5) = 0.0003494028541)
We can also plot these values to get a better understanding of the dependability of the Moroccan signaling system as given in Figure 2. It can be observed from the plot that initially the probability of failure is very low but as the time passes, in hours, the failure probability gradually increases and at 2,000 hours the failure becomes absolutely certain, i.e., with a probability 1.
## B. Formal Importance Measure Analysis
As described in Section IV, the importance measure analysis requires the given system structure function to be coherent in nature. Therefore, we start by formally verifying the conditions of a coherent system for the railway signaling system MCS, described in Lemma 2, in HOL as:
## Theorem 7: /turnstileleft
```
Theory 7: F
prob_space p ^
coherent_state_vec (íza. a = {}) (FLAT
[wL p [x3;x4;x5;x6] t;
wL p [x9;x13;x15;x11] t;...;
wL p [x10;x14;x16;x12] t;
```
<details>
<summary>Image 4 Details</summary>
### Visual Description
## Line Graph: Probability of Failure Over Time
### Overview
The image depicts a line graph illustrating the relationship between time (t) and the probability of failure. The x-axis represents time in discrete intervals (t=1, t=2, ..., t=2000), while the y-axis represents the probability of failure, ranging from 0 to 1. The line shows a consistent upward trend, indicating an increasing probability of failure as time progresses.
### Components/Axes
- **X-axis (Time)**: Labeled "Time" with discrete markers at t=1, t=2, t=5, t=10, t=50, t=100, t=1000, and t=2000. The scale is linear, with equal spacing between intervals.
- **Y-axis (Probability of Failure)**: Labeled "Probability of Failure" with values ranging from 0.0000145 to 1. The scale is logarithmic, as the intervals between values increase exponentially (e.g., 0.0000145, 0.0000574, 0.000349, etc.).
- **Legend**: No explicit legend is present in the image. The line is black with circular markers, but no color-coded categories or labels are provided.
- **Data Points**: Black circular markers are plotted at each time interval, connected by a solid black line.
### Detailed Analysis
- **Data Points**:
- t=1: 0.0000145
- t=2: 0.0000574
- t=5: 0.000349
- t=10: 0.00133
- t=50: 0.0234
- t=100: 0.0645
- t=1000: 0.55
- t=2000: 0.999 (approximate, as the line approaches 1)
- **Trend**: The line exhibits a **logarithmic/exponential growth pattern**, with the probability of failure increasing rapidly after t=100. The slope becomes steeper as time progresses, suggesting a nonlinear relationship between time and failure probability.
### Key Observations
1. **Exponential Growth**: The probability of failure increases dramatically after t=100, reaching ~0.55 at t=1000 and approaching 1 by t=2000.
2. **Initial Stability**: At t=1–10, the probability remains extremely low (<0.001), indicating minimal risk in the early stages.
3. **Critical Threshold**: The probability crosses 0.5 at t=1000, suggesting a 50% chance of failure by this point.
4. **Asymptotic Behavior**: The line approaches 1 asymptotically, implying the probability of failure approaches certainty as time extends beyond t=2000.
### Interpretation
The graph demonstrates that the system's failure probability grows exponentially over time, with a critical threshold of 50% failure risk occurring at t=1000. This suggests that the system becomes increasingly unreliable as it ages, with failure becoming nearly inevitable by t=2000. The absence of a legend implies a single data series, but the lack of contextual information (e.g., system type, failure criteria) limits deeper analysis. The logarithmic y-axis emphasizes the rapid escalation of risk, highlighting the importance of proactive maintenance or replacement strategies for systems operating beyond t=1000.
</details>
Fig. 2. Plot for Probability of Failure of Signaling System at Moroccan Level Crossing
```
Theorem 8: |-
coherent_state_vec (íza. a = p_space p) (FLAT
[wL p [x3;x4;x5;x6] t;
wL p [x9;x13;x15;x11] t::;;
wL p [x10;x14;x16;x12] t;
wL p [x7;x8;x1;x2] t]) =>
(prob p
(φ (λb.
FTree p((OR of
(Aa. AND (gate_list a))) b))
wL p [x3;x4;x5;x6] t;
wL p [x9;x13;x15;x11] t;;...
wL p [x10;x14;x16;x12] t;
wL p [x7;x8;x1;x2] t]) = 1)
```
```
Theorem 9: |-
prob_space p ^
(!t. in_events p (FLAT
[wL p [x3;x4;x5;x6] t;
wL p [x9;x13;x15;x11] t;...;
wL p [x10;x14;x16;x12] t;
wL p [x7;x8;x1;x2] t])) ^
t1 < t2 =>
prob p
(p (Ab.
FTree p((OR of
(Aa. AND (gate_list a))) b))
wL p [x9;x13;x15;x11] t1;...;
wL p [x10;x14;x16;x12] t1;
wL p [x7;x8;x1;x2] t1]) <
prob p
(p (Ab.
FTree p ((OR of
```
```
```
```
(lambda. AND (gate_list a))) b))
[ωL p [x3;x4;x5;x6] t2;
ωL p [x9;x13;x15;x11] t2;;...;
ωL p [x10;x14;x16;x12] t2;
ωL p [x7;x8;x1;x2] t2])
```
It can be seen that Theorems 7-8 are formally verified based on a very straight-forward utilization of Theorems 1-2, described in Section IV-A, on a given list of railway signaling MCS. Similary, Theorem 9 is formally verified by utilizing Theorem 3 by discharging the assumption mem\_subset\_vec based on the fact that by increasing the time-of-failures, i.e., t1 ≤ t2 , the corresponding failure probabilities also monotonically increase.
## C. Formal Birnbaum Importance Measure Analysis
After formally satisfying the conditions for coherent system on the railway signaling system failure model, we can now determine the Birnbaum importance measure of any component of the railway signaling system. For illustration purposes, we describe the formal importance measure analysis of an alarm failure ( x 9 ) in the railway signaling system by utilizing Definition 4 and the FT model, described in Definition 8, in HOL as:
```
HOL as:
Definition 9: |- I$_{B}$ p x1 x2 x3 ::: x16 t =
I$_{B}$ p 0
(lambda. FTree p (OR [OR ([w p x3 t;w p x4 t])
OR ([w p x5 t;w p x6 t]);
AND [OR b ;
OR ([w p x13 t;w p x14 t]);
OR ([w p x15 t;w p x16 t]);
OR ([w p x11 t;w p x12 t])];
OR ([w p x7 t;w p x8 t]);
OR ([w p x1 t;w p x2 t])] )
(([w p x9 t;w p x10 t]))
```
The above model can also be used to quantitatively analyze the Birnbaum importance of alarm failure by associating the exponential distribution to each component of the railway signaling system as:
```
signaling system as:
Theorem 10: |- \forall p x1 x2 ··· x16 c1 c2 ··· c16 t.
[A1]: 0 ≤ t ^
[A2]: prob_space p ^
[A3]: mutual_indep p ( \omega L p
[x1; x2; ... ; x16] t) ^
[A4]: in_events p ( \omega L p
[x1; x2; ... ; x16] t) ^
[A5]: exp_dist_list p [x1;x2; ... ;x16]
[c1;c2;...;;c16] =>
(I 9 β p x1 x2 x3 ··· x16 t =
e - \lambda c3 *t * e - \lambda c4 *t * e - \lambda c5 *t * e - \lambda c6 *t *
e - \lambda c7 *t * e - \lambda c8 *t * e - \lambda c2 *t * e - \lambda c1 *t * e - \lambda c10 *t *
(1 - e - \lambda c13 *t * e - \lambda c14 *t ) *
(1 - e - \lambda c15 *t * e - \lambda c16 *t ) *
(1 - e - \lambda c11 *t * e - \lambda c12 *t ))
```
The assumptions of the above theorem is quite similar to the ones used in Theorem 6. It can be observed from the conclusion of Theorem 9 that the importance of alarm failure component ( x 9 ) is calculated from the failure probabilities of other components in the FT model.
Similarly, we can also determine the Fussell-Vesely importance measure for the alarm component by using Definition 5 in HOL as follows:
```
Similarly, we can also determine the Fussell-Vessely impor-tance measure for the alarm component by using Definition 5 in HOL as follows:
Theorem 11: |- \p x1 x2 ... x16 c1 c2 ... c16 t.
[A1]: 0 < t ^ A
[A2]: prob_space p ^ A
[A3]: mutual_indep p ( \omega L p
[x1; x2; ... ; x16] t) ^ A
[A4]: in_events p ( \omega L p
[x1; x2; ... ; x16] t) ^ A
[A5]: exp_dist_list p [x1;x2; ... ;x16]
[c1;c2;...;c16] =>
(I_FV_9 p x1 x2 x3 ... x16 t =
(l -
e(-(\c3*t)) * e(-(\c4*t)) * e(-(\c5*t)) *
...
(l - e(-(\c9*t)) * e(-(\c10*t))) *
(l - e(-(\c13*t)) * e(-(\c14*t))) *
(l - e(-(\c15*t)) * e(-(\c16*t))) *
(l - e(-(\c11*t)) * e(-(\c12*t))) )
(l -
e(-(\c3*t)) * e(-(\c4*t)) * e(-(\c5*t)) *)
...
(l - e(-(\c13*t)) * e(-(\c14*t))) *
(l - e(-(\c15*t)) * e(-(\c16*t))) *
(l - e(-(\c11*t)) * e(-(\c12*t))) ) /
(l -
e(-(\c3*t)) * e(-(\c4*t)) * e(-(\c5*t)) *)
...
(l - e(-(\c9*t)) * e(-(\c10*t))) *
(l - e(-(\c13*t)) * e(-(\c14*t))) *
(l - e(-(\c15*t)) * e(-(\c16*t))) *)
(l - e(-(\c11*t)) * e(-(\c12*t))) )
```
By using the above-mentioned approach, we can formally determine the Reduction Worth (RW) and Achievement Worth (AW) importance measures, given in Equation 6. Next, we conduct the formal relative importance measure analyses of relative importance among alarm and vehicle failure, using Theorem 4, as follows:
```
Theorem 4, as follows:
Theorem 12: |- \p x1 x2 ... x16 c1 c2 ... c16 t.
[A1]: 0 ≤ t ^
[A2]: prob_space p ^
[A3]: mutual_indep p (wL p
[x1; x2; :::; x16] t) ^
[A4]: in_events p (wL p
[x1; x2; :::; x16] t) ^
[A5]: exp_dist_list p [x1;x2; ::: ;x16]
[c1;c2;;:;c16] ^
[A6]: fail_rate_pos [c1;c2;;:;c16] ^
[A7]: c9 ≤ c1 =>
I 9 \p x1 x2 x3 ::: x16 t \leq
I 1 \p x1 x2 x3 ::: x16 t
```
where the function fail\_rate\_pos , in assumption (A6), ensures that the given list of failure rates must be positive. It can be implied from assumption (A7) that the Birnbaum relative importance of any two components in a system is related by their failure rates relationship. In other words, a component with higher failure rate is highly critical in a FT model (structure function) compared to a component with lower failure rate. The proof of Theorem 12 is based on Theorem 4 and some fundamental facts of probability theory. The HOL proof script of Theorems 6-12, which can be downloaded from [24], took about 1200 lines of HOL code and about 24 man-hours.
It is quite evident that our proposed HOL-based formalization approach provides the required rigor to the importance measure properties about system components compared to [10]. Also, all the necessary conditions are accompanying the formally verified properties. Most importantly, the formal relative importance measure analysis reveals that the relative importance of any pair of components is related according to their failure rates (Theorem 12). In other words, we can accurately analyze the components' importance, due to the sound theorem proving approach, without using the traditional methods of ranking the system components for large systems. By conducting the formal importance analysis of the railway signaling system at a Moroccan LC, we believe that our proposed approach provides a sound framework to reliability design engineers to meet the quality standards of their safetycritical systems.
## VI. CONCLUSION
In this paper, we formalized the commonly used importance measures, such as Birnbaum, Fussely-vesely, Reduction worth and Achievement worth, in HOL theorem proving. We also formalized Meng's approach of obtaining the relative importance measure among any pair of system components. For illustration purposes, we conducted the formal importance measure analysis of a signaling system at a Moroccan level crossing consisting of traffic lights, programmable logic controllers and alarms, within the HOL theorem proving environment. We plan to extend the formalization of Fussell-vesely importance measure to obtain the relative importance of system components. Just like the Birnbaum importance measure, it has great potential to highlight the critical components without running the computationally expensive simulations.
## REFERENCES
- [1] W. Kuo and X. Zhu, Importance Measures in Reliability, Risk, and Optimization: Principles and Applications . John Wiley & Sons, 2012.
- [2] P. Rooney, 'Microsoft's CEO: 80-20 Rule Applies to Bugs, Not Just Features,' 2019. [Online]. Available: https://www.crn.com/news/security/18821726/ microsofts-ceo-80-20-rule-applies-to-bugs-not-just-features.htm
- [3] Z. W. Birnbaum, 'On the importance of Different Components in a Multicomponent System,' University of Washington, Seatle, Washington, USA, Tech. Rep., 1968. [Online]. Available: http://www. dtic.mil/dtic/tr/fulltext/u2/670563.pdf
- [4] J. F. Espiritu, D. W. Coit, and U. Prakash, 'Component Criticality Importance Measures for the Power Industry,' Electric Power Systems Research , vol. 77, no. 5-6, pp. 407-420, 2007.
- [5] ReliaSoft, 2019. [Online]. Available: https://www.weibull.com/hotwire/ issue66/relbasics66.htm
- [6] P. J. Boland, F. Proschan, and Y. L. Tong, 'Optimal Arrangement of Components via Pairwise Rearrangements,' Naval Research Logistics , vol. 36, no. 6, pp. 807-815, 1989.
- [7] F. C. Meng, 'Comparing Birnbaum Importance Measure of System Components,' Probability in the Engineering and Informational Sciences , vol. 18, no. 2, pp. 237-245, 2004.
- [8] J. Harrison, Handbook of Practical Logic and Automated Reasoning . Cambridge University Press, 2009.
- [9] IEC, 'International Electrotechnical Commission, 61025 Fault Tree Analysis,' 2006. [Online]. Available: https://webstore.iec.ch/ publication/4311
- [10] J. Boudnnaya, A. Mkhida, and M. Sallak, 'A Dependability Analysis of a Moroccan Level Crossing Based on Fault Tree Analysis and Importance Measures,' in MOdeling, Optimization and SIMlation , 2014, pp. 1-5, https://recif.hds.utc.fr/wp-content/uploads/2014/11/ MOSIM\_2014\_1.pdf.
- [11] HOL Interactive Theorem Prover, 2019. [Online]. Available: https:// hol-theorem-prover.org/
- [12] W. Ahmad, 'Formal Dependability Analysis using Higher-order-logic Theorem Proving,' PhD Thesis, National University of Sciences and Technology, Islamabad, Pakistan, 2017.
- [13] K. S. Trivedi, Probability and Statistics with Reliability, Queuing and Computer Science Applications . John Wiley and Sons Ltd., 2002.
- [14] W. Ahmed, O. Hasan, and S. Tahar, 'Formalization of Reliability Block Diagrams in Higher-order Logic,' Journal of Applied Logic , vol. 18, pp. 19-41, 2016.
- [15] W. Ahmad, O. Hasan, and S. Tahar, Handbook of RAMS in Railways: Theory and Practice . Taylor and Francis, 2018, ch. Formal Reliability Analysis of Railway Systems using Theorem Proving Technique, pp. 651-668.
- [16] W. Ahmad and O. Hasan, 'Towards Formal Fault Tree Analysis Using Theorem Proving,' in Intelligent Computer Mathematics , ser. LNCS. Springer, 2015, vol. 9150, pp. 39-54.
- [17] W. Ahmad and O. Hasan, 'Formalization of Fault Trees in Higherorder Logic: A Deep Embedding Approach,' in Dependable Software Engineering: Theories, Tools, and Applications , ser. LNCS. Springer, 2016, vol. 9984, pp. 264-279.
- [18] M. J. Gordon and T. F. Melham, Introduction to HOL A Theorem Proving Environment for Higher-order Logic . Cambridge University Press, 1993.
- [19] A. Church, 'A Formulation of the Simple Theory of Types,' Journal of Symbolic Logic , vol. 5, pp. 56-68, 1940.
- [20] R. Milner, 'A Theory of Type Polymorphism in Programming,' Journal of Computer and System Sciences , vol. 17, pp. 348-375, 1977.
- [21] T. Mhamdi, O. Hasan, and S. Tahar, 'On the Formalization of the Lebesgue Integration Theory in HOL,' in Interactive Theorem Proving , ser. LNCS. Springer, 2011, vol. 6172, pp. 387-402.
- [22] W. Ahmad, O. Hasan, S. Tahar, and M. S. Hamdi, 'Towards the Formal Reliability Analysis of Oil and Gas Pipelines,' in Intelligent Computer Mathematics , ser. LNCS. Springer, 2014, vol. 8543, pp. 30-44.
- [23] J. D. Andrews and S. C. Beeson, 'Birnbaum's Measure of Component Importance for Noncoherent Systems,' IEEE Transcation on Reliability , vol. 52, no. 2, pp. 213-219, 2003.
- [24] W. Ahmad, 'On the Formalization of Importance Measures using HOL Theorem Proving,' 2019. [Online]. Available: https://github.com/ahmedwaqar/Formal-Dependability/tree/ importance\_measures/Importance\_Measures