## 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
\n
## Table: Formalization of FT Gates
### Overview
The image presents a table detailing the formalization of fundamental logic gates (AND, OR, NAND, NOR, XOR). Each row corresponds to a specific gate, displaying its symbol, and a corresponding mathematical or logical expression.
### Components/Axes
The table has two columns:
1. **FT Gates:** This column displays the schematic symbol for each logic gate.
2. **Formalization:** This column provides the logical or mathematical expression representing the gate's function.
### Content Details
Here's a detailed transcription of the table's content, row by row:
* **AND:**
* Symbol: Standard AND gate symbol.
* Formalization: `¬ ∀ p L1 L2. AND_FT_gate p L1 L2 = FTree p (AND (gate_list L1))`
* **OR:**
* Symbol: Standard OR gate symbol.
* Formalization: `¬ ∀ p L. OR_FT_gate p L = FTree p (OR (gate_list L))`
* **NAND:**
* Symbol: Standard NAND gate symbol.
* Formalization: `¬ ∀ p L1 L2. NAND_FT_gate p L1 L2 = FTree p (AND (gate_list (compl_list p ++ L2)))`
* **NOR:**
* Symbol: Standard NOR gate symbol.
* Formalization: `¬ ∀ p L. NOR_FT_gate p L = FTree p (NOT (OR (gate_list L)))`
* **XOR:**
* Symbol: Standard XOR gate symbol.
* Formalization: `¬ ∀ p A B. XOR_FT_gate p A B = FTree p (OR [AND [NOT A; B]; AND [A; NOT B]])`
### Key Observations
* The formalizations utilize a notation involving `FTree`, `AND`, `OR`, `NOT`, `compl_list`, and `gate_list`.
* The expressions appear to define the gate's behavior in terms of a tree structure (`FTree`) and operations on lists of inputs (`gate_list`).
* The `compl_list` function in the NAND gate formalization suggests a negation or complement operation on the input list.
* The XOR gate formalization is more complex, involving nested `AND` and `OR` operations with negated inputs.
### Interpretation
This table provides a formal, potentially computational, representation of basic logic gates. The use of `FTree` suggests a hierarchical or tree-based approach to representing the gate's functionality. The expressions are likely intended for use in a system that can manipulate and evaluate these logical structures, perhaps for automated theorem proving, circuit verification, or logic synthesis. The notation is somewhat abstract and requires understanding of the underlying mathematical or logical framework to fully interpret. The use of `¬ ∀` suggests a universal quantification with negation, indicating a rule or definition that holds for all possible inputs. The expressions are not standard Boolean algebra but a more specialized formalization. The table is a technical document aimed at someone familiar with formal logic and potentially functional programming concepts.
</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
## Data Table: Boolean Function Reliability Expressions
### Overview
The image presents a data table comparing mathematical expressions for the reliability of various Boolean functions (AND, OR, NAND, NOR, XOR) with their corresponding theorems' conclusions. The table has two columns: "Mathematical Expressions" and "Theorem's Conclusion". Each row represents a different Boolean function and provides its reliability expression and the associated theorem.
### Components/Axes
The table is structured with rows representing different Boolean functions:
* AND
* OR
* NAND
* NOR
* XOR
Each row has two columns:
* **Mathematical Expressions:** Contains the probabilistic expression for the function's reliability.
* **Theorem's Conclusion:** Contains the logical conclusion or theorem related to the function.
### Detailed Analysis or Content Details
**1. AND (t)**
* **Mathematical Expression:** Pr(∩ Ai(t)) from i=2 to N = ∏ Fi(t) from i=2 to N
* **Theorem's Conclusion:** ∀ V p L1 L2. (prob p (AND_FT_gate p L) = list_prod (list_prob p p))
**2. OR (t)**
* **Mathematical Expression:** Pr(∪ Ai(t)) from i=2 to N = 1 - ∏ (1 - Fi(t)) from i=2 to N
* **Theorem's Conclusion:** ∀ V p L1 L2. (prob p (OR_FT_gate p L) = 1 - list_prod (one_minus_list (list_prob p L)))
**3. NAND (t)**
* **Mathematical Expression:** Pr(∩ Āi(t) ∩ Ai(t)) from j=k to N = ∏ (1 - Fi(t)) from i=2 to k * ∏ Fj(t) from j=k to N
* **Theorem's Conclusion:** ∀ V p L1 L2. (prob p (NAND_FT_gate p L1 L2) = list_prod (list_prob p L1) * (compl_list p L1) * list_prod (list_prob p L2))
**4. NOR (t)**
* **Mathematical Expression:** 1 - FOR(t) = ∏ (1 - Fi(t)) from i=2 to N
* **Theorem's Conclusion:** ∀ V p L. (prob p (NOR_FT_gate p L) = list_prod (one_minus_list (list_prob p L)))
**5. XOR (t)**
* **Mathematical Expression:** Pr(Ā(t)B(t) ∪ A(t)B̄(t)) = (1 - FA(t))FB(t) + FA(t)(1 - FB(t))
* **Theorem's Conclusion:** ∀ V 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 table provides a direct mapping between probabilistic reliability expressions and their corresponding logical theorems for common Boolean functions.
* The mathematical expressions utilize probability notation (Pr), intersection (∩), union (∪), and product notation (∏).
* The theorem's conclusions use a formal notation involving "∀" (for all), "V" (variable), "p" (probability), "L" (list), and function-specific gate names (AND_FT_gate, OR_FT_gate, etc.).
* The expressions for NAND and XOR are more complex than those for AND, OR, and NOR.
### Interpretation
This table demonstrates the relationship between Boolean algebra and probability theory in the context of reliability analysis. It shows how the reliability of a Boolean function can be expressed mathematically using probability, and how this relates to the logical properties of the function. The use of "FT_gate" suggests these are fault-tolerant gate implementations. The table is likely intended for engineers or researchers working on the design and analysis of reliable digital systems. The formal notation in the "Theorem's Conclusion" column suggests a formal verification or automated reasoning context. The expressions provide a way to calculate the probability of a function being in a specific state, given the probabilities of its inputs. The table is a concise reference for translating between logical function definitions and their probabilistic reliability characteristics.
</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
\n
## Diagram: Fault Tree Analysis
### Overview
The image depicts a fault tree diagram, a top-down, deductive failure analysis method. It visually represents the logical relationships between a system's failure (the "Top Event") and the events that can cause it. The diagram uses logic gates (AND, OR) to connect events, showing how combinations of lower-level failures can lead to the top-level failure.
### Components/Axes
The diagram consists of:
* **Top Event:** A rectangular box labeled "Top Event" at the top center.
* **Logic Gates:** OR gates (curved shape) and AND gates (pointed shape) connecting events.
* **Basic Events:** Circles labeled "x1" through "x16" representing potential failures at the lowest level.
* **Connecting Lines:** Lines indicating the flow of logic and dependencies between events and gates.
### Detailed Analysis or Content Details
The diagram can be described level by level, starting from the top:
1. **Level 1 (Top Event):** The "Top Event" is connected to three OR gates. This means the Top Event can occur if *any* of the three events connected to these OR gates occur.
2. **Level 2:**
* The first OR gate is connected to two basic events: x1 and x2.
* The second OR gate is connected to two basic events: x3 and x4.
* The third OR gate is connected to two basic events: x5 and x6.
3. **Level 3:**
* The output of the first OR gate (x1 or x2) is connected to an AND gate along with the output of the second OR gate (x3 or x4). This AND gate means that *both* (x1 or x2) *and* (x3 or x4) must occur for the next level to be triggered.
* The output of the third OR gate (x5 or x6) is connected to an AND gate with the output of the AND gate from the previous step.
4. **Level 4:**
* The output of the AND gate (from Level 3) is connected to three OR gates.
* The first OR gate is connected to two basic events: x7 and x8.
* The second OR gate is connected to two basic events: x9 and x10.
* The third OR gate is connected to two basic events: x11 and x12.
5. **Level 5:**
* The output of the first OR gate (x7 or x8) is connected to an AND gate.
* The output of the second OR gate (x9 or x10) is connected to an AND gate.
* The output of the third OR gate (x11 or x12) is connected to an AND gate.
6. **Level 6:**
* Each of the three AND gates (from Level 5) is connected to two basic events.
* The first AND gate is connected to x13 and x14.
* The second AND gate is connected to x15 and x16.
* The third AND gate is connected to no events.
### Key Observations
* The diagram is symmetrical in its structure, with branching occurring at multiple levels.
* The use of both OR and AND gates indicates a complex relationship between the basic events and the top event.
* The diagram shows that the Top Event can occur through multiple pathways, some requiring multiple failures to occur simultaneously (AND gates), while others require only one failure (OR gates).
* The final AND gate on the right side of the diagram is connected to no events, which is an anomaly.
### Interpretation
This fault tree diagram is a visual representation of a system's potential failure modes. It allows engineers to identify critical components and events that contribute most significantly to the overall system failure. By analyzing the diagram, they can prioritize efforts to improve system reliability and safety. The presence of both OR and AND gates highlights the need to address both single-point failures (OR gates) and combinations of failures (AND gates). The anomaly of the unconnected AND gate suggests a potential error in the diagram or a missing component in the analysis. The diagram suggests that the Top Event is dependent on a complex interplay of events, and mitigating the risk of the Top Event requires addressing failures at multiple levels of the system. The diagram is a tool for risk assessment and mitigation, helping to identify vulnerabilities and improve system resilience.
</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
\n
## Chart: Probability of Failure vs. Time
### Overview
The image presents a line graph illustrating the relationship between time and the probability of failure. The graph shows a generally increasing trend, indicating that the probability of failure rises as time progresses. The x-axis represents time, and the y-axis represents the probability of failure. Specific time points are marked along the x-axis.
### Components/Axes
* **X-axis:** Labeled "Time". Markers are present at t=1, t=2, t=5, t=10, t=50, t=100, t=1000, and t=2000.
* **Y-axis:** Labeled "Probability of Failure". The scale is logarithmic, 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 representing the probability of failure over time.
### Detailed Analysis
The line begins at approximately (t=1, Probability of Failure ≈ 0.0000145) and increases steadily. The slope of the line is not constant, indicating a non-linear relationship.
Here's a breakdown of approximate data points:
* (t=1, Probability of Failure ≈ 0.0000145)
* (t=2, Probability of Failure ≈ 0.0000574)
* (t=5, Probability of Failure ≈ 0.000349)
* (t=10, Probability of Failure ≈ 0.00133)
* (t=50, Probability of Failure ≈ 0.0234)
* (t=100, Probability of Failure ≈ 0.0645)
* (t=1000, Probability of Failure ≈ 0.55)
* (t=2000, Probability of Failure ≈ 1)
The line exhibits a relatively slow increase from t=1 to t=100, then a steeper increase from t=100 to t=2000.
### Key Observations
* The probability of failure is very low at small time values (t=1 to t=10).
* The rate of increase in the probability of failure accelerates as time increases.
* At t=2000, the probability of failure reaches 1 (certainty).
* The logarithmic scale on the y-axis emphasizes the initial low probabilities and the subsequent rapid increase.
### Interpretation
The chart likely represents the reliability or failure rate of a system or component over time. The increasing probability of failure suggests that the system is more likely to fail as it ages. The non-linear relationship indicates that the failure rate is not constant; it increases with time, potentially due to wear and tear, degradation of materials, or accumulation of stress. The chart could be used to estimate the expected lifespan of the system or to schedule maintenance and replacements. The steep increase in failure probability towards the end of the time scale suggests a "wear-out" phase, where the system is nearing the end of its useful life. The logarithmic scale is used to effectively visualize the wide range of probabilities, from very small initial values to near certainty.
</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