## 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
## Logic Gate Diagram: FT Gates Formalization
### Overview
The image presents a table describing several fundamental logic gates (AND, OR, NAND, NOR, XOR) using both their symbolic representation and a formalization using a functional notation. The table is organized into two columns: "FT Gates" showing the gate symbol, and "Formalization" providing the logical expression.
### Components/Axes
* **Table Header:**
* Column 1: "FT Gates" - Contains the logic gate symbols.
* Column 2: "Formalization" - Contains the formal representation of the logic gates.
* **Logic Gates:** The following logic gates are represented: AND, OR, NAND, NOR, XOR.
* **Formalization Notation:** The formalization uses symbols like ∀ (for all), p, L, L1, L2, A, B, FTree, AND, OR, NOT, gate_list, compl_list, ++.
### Detailed Analysis
The table consists of 5 rows, each representing a different logic gate.
* **AND Gate:**
* Symbol: Standard AND gate symbol with 'n' inputs indicated by dashed lines. Inputs are labeled '1' and 'n'.
* Formalization: "∀ p L1 L2. AND\_FT\_gate p L1 L2 = FTree p (AND (gate\_list L))"
* **OR Gate:**
* Symbol: Standard OR gate symbol with 'n' inputs indicated by dashed lines. Inputs are labeled '1' and 'n'.
* Formalization: "∀ p L. OR\_FT\_gate p L = FTree p (OR (gate\_list L))"
* **NAND Gate:**
* Symbol: Standard NAND gate symbol with 'k' inputs indicated by dashed lines. Inputs are labeled '-1' and '-k'.
* Formalization: "∀ p L1 L2. NAND\_FT\_gate p L1 L2 = FTree p (AND (gate\_list (compl\_list p L1 ++ L2)))"
* **NOR Gate:**
* Symbol: Standard NOR gate symbol with 'n' inputs indicated by dashed lines. Input is labeled '-1' and '-n'.
* Formalization: "∀ p L. NOR\_FT\_gate p L = FTree p (NOT (OR (gate\_list L)))"
* **XOR Gate:**
* Symbol: Standard XOR gate symbol with two inputs. Inputs are labeled '-1' and '-2'.
* Formalization: "∀ p A B. XOR\_FT\_gate p A B = FTree p (OR [AND [NOT A; B]; AND [A; NOT B]])"
### Key Observations
* The formalization uses a functional notation to represent the logic gates.
* The number of inputs is explicitly indicated for AND, OR, NAND, and NOR gates, while XOR is shown with two inputs.
* The formalization includes functions like `FTree`, `gate_list`, and `compl_list`, suggesting a tree-based representation or manipulation of gates.
* The NAND gate formalization includes `compl_list`, indicating a complement operation.
* The XOR gate formalization explicitly shows the logical expression (A'B + AB').
### Interpretation
The image provides a formal representation of common logic gates, bridging the gap between their symbolic representation and a functional or algebraic description. This type of formalization is useful in automated reasoning, circuit verification, and logic synthesis. The use of functions like `FTree` and `gate_list` suggests a more abstract or hierarchical representation of logic circuits, potentially used in formal verification or synthesis tools. The formalization allows for a precise and unambiguous definition of each gate's behavior, which is essential for automated manipulation and analysis.
</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
## Mathematical Expressions and Theorem's Conclusion
### Overview
The image presents a table comparing mathematical expressions for logical operations (AND, OR, NAND, NOR, XOR) with their corresponding theorem conclusions. The left column displays the mathematical formulas, while the right column shows the theorem's conclusion related to each logical operation.
### Components/Axes
The table has two columns:
* **Mathematical Expressions**: Contains mathematical formulas for FAND, FOR, FNAND, FNOR, and FXOR.
* **Theorem's Conclusion**: Contains logical expressions and functions related to the mathematical expressions.
### Detailed Analysis
**Mathematical Expressions Column:**
* **FAND(t)**:
* `FAND(t) = Pr(∩(i=2 to N) Ai(t))`
* `= Π(i=2 to N) Fi(t)`
* **FOR(t)**:
* `FOR(t) = Pr(∪(i=2 to N) Ai(t))`
* `= 1 - Π(i=2 to N) (1 - Fi(t))`
* **FNAND(t)**:
* `FNAND(t) = Pr(∩(i=2 to k) Āi(t) ∩ ∩(j=k to N) Aj(t))`
* `= Π(i=2 to k) (1 - Fi(t)) * Π(j=k to N) (Fj(t))`
* **FNOR(t)**:
* `FNOR(t) = 1 - FOR(t) = Π(i=2 to N) (1 - Fi(t))`
* **FXOR(t)**:
* `FXOR(t) = Pr(Ā(t)B(t) ∪ A(t)B̄(t))`
* `= (1 - FA(t))FB(t) + FA(t)(1 - FB(t))`
**Theorem's Conclusion Column:**
* **AND**:
* `∀ p L1 L2.`
* `(prob p (AND_FT_gate L) = list_prod (list_prob p L))`
* **OR**:
* `∀ p L1 L2.`
* `(prob p (OR_FT_gate p L) = 1 - list_prod (one_minus_list (list_prob p L)))`
* **NAND**:
* `∀ 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))`
* **NOR**:
* `∀ p L.`
* `(prob p (NOR_FT_gate p L) = list_prod (one_minus_list (list_prob p L)))`
* **XOR**:
* `∀ 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))`
### Key Observations
* The mathematical expressions define the probability of AND, OR, NAND, NOR, and XOR operations in terms of events A and B.
* The theorem's conclusions provide logical representations of these operations, likely within a formal system or programming context.
* The use of `list_prod`, `list_prob`, and `one_minus_list` suggests these are functions operating on lists of probabilities.
* The NAND gate conclusion uses `compl_list`, suggesting a function that complements a list of probabilities.
### Interpretation
The table bridges the gap between probability theory and logical operations, providing a formal representation of how these operations can be expressed and reasoned about within a probabilistic framework. The theorem's conclusions likely serve as a basis for implementing these logical operations in systems that deal with probabilities, such as fault-tolerant systems or probabilistic programming languages. The use of list operations suggests that these operations can be generalized to handle multiple inputs.
</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
## Fault Tree Diagram: Top Event Analysis
### Overview
The image presents a fault tree diagram, a top-down, deductive failure analysis used to determine how systems can fail, identify the best ways to reduce risk, and determine (or get a feeling for) event rates of a safety accident or a particular system level (functional) failure. The diagram starts with a "Top Event" and branches down through a series of logic gates (AND, OR) to identify potential causes or contributing factors, represented by basic events (x1, x2, ..., x16).
### Components/Axes
* **Top Event:** A rectangular box at the top of the diagram labeled "Top Event".
* **Basic Events:** Represented by circles labeled x1 through x16.
* **Logic Gates:**
* **OR Gate:** An upside-down U-shaped symbol. The output event occurs if at least one of the input events occurs.
* **AND Gate:** A U-shaped symbol. The output event occurs only if all input events occur.
* **Connecting Lines:** Lines connecting events and gates, indicating the flow of logic.
### Detailed Analysis
The diagram can be broken down into levels, starting from the top:
1. **Level 1:** The "Top Event" is connected to an OR gate. This OR gate has three inputs.
2. **Level 2:** The three inputs to the OR gate are:
* An OR gate connected to basic events x3 and x4.
* An OR gate connected to the next level.
* An OR gate connected to basic events x1 and x2.
3. **Level 3:** The central OR gate from Level 2 is connected to:
* An AND gate connected to basic events x5 and x6.
* An AND gate connected to basic events x8 and x7.
4. **Level 4:** The outputs of the AND gates from Level 3 feed into an AND gate.
5. **Level 5:** The output of the AND gate from Level 4 feeds into an OR gate. This OR gate has two inputs.
6. **Level 6:** The two inputs to the OR gate are:
* An OR gate connected to basic events x9 and x10.
* An OR gate connected to the next level.
* An OR gate connected to basic events x11 and x12.
7. **Level 7:** The central OR gate from Level 6 is connected to:
* An AND gate connected to basic events x13 and x14.
* An AND gate connected to basic events x15 and x16.
### Key Observations
* The diagram uses a combination of OR and AND gates to model the relationships between events.
* The diagram is structured hierarchically, with the "Top Event" at the root and basic events at the leaves.
* The diagram includes 16 basic events (x1 to x16).
### Interpretation
The fault tree diagram visually represents the logical relationships between potential causes and a specific "Top Event." By tracing the paths from the basic events (x1-x16) through the logic gates, one can identify the combinations of failures that could lead to the "Top Event." The use of both OR and AND gates allows for modeling situations where a single failure can cause the "Top Event" (OR gate) or where multiple failures must occur simultaneously (AND gate). This type of analysis is crucial for risk assessment and safety engineering, as it helps to pinpoint critical vulnerabilities in a system and prioritize mitigation efforts.
</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 Chart: Probability of Failure vs. Time
### Overview
The image is a line chart illustrating the probability of failure over time. The x-axis represents time (t), and the y-axis represents the probability of failure. The chart shows an increasing trend in the probability of failure as time increases.
### Components/Axes
* **X-axis:** Time (t) with markers at t=1, t=2, t=5, t=10, t=50, t=100, t=1000, and t=2000.
* **Y-axis:** Probability of Failure with markers at 0.0000145, 0.0000574, 0.000349, 0.00133, 0.0234, 0.0645, 0.55, and 1.
* **Data Series:** A single black line with data points indicating the probability of failure at different time intervals.
### Detailed Analysis
The data series (black line) shows the following approximate values:
* At t=1, Probability of Failure ≈ 0.0000145
* At t=2, Probability of Failure ≈ 0.0000574
* At t=5, Probability of Failure ≈ 0.000349
* At t=10, Probability of Failure ≈ 0.00133
* At t=50, Probability of Failure ≈ 0.0234
* At t=100, Probability of Failure ≈ 0.0645
* At t=1000, Probability of Failure ≈ 0.55
* At t=2000, Probability of Failure ≈ 1
The line slopes upward, indicating an increasing probability of failure as time increases. The rate of increase appears to be higher in the later time intervals (t=1000 to t=2000) compared to the earlier intervals (t=1 to t=100).
### Key Observations
* The probability of failure increases with time.
* The rate of increase in the probability of failure is not constant; it appears to accelerate at later times.
* The y-axis scale is not linear, allowing for representation of both very small and relatively large probabilities of failure.
### Interpretation
The chart suggests that the likelihood of failure increases over time, and the rate of failure accelerates as time progresses. This could represent the wear and tear of a component or system, where the initial failures are rare, but as time goes on, the probability of failure increases significantly. The non-linear y-axis scale is necessary to visualize the wide range of probability values, from very small initial failure rates to near-certain failure at later times.
</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