Adnan Rashid, School of Electrical Engineering and Computer Science (SEECS)
National University of Sciences and Technology (NUST), Islamabad, Pakistan

# Towards the Formal Performance Analysis of Multistate Coherent Systems using
HOL Theorem Proving

Shahid Ali Murtza  Waqar Ahmed  Adnan Rashid and Osman Hasan  School of
Electrical Engineering and Computer Science (SEECS)
National University of Sciences and Technology (NUST), Islamabad, Pakistan
<EMAIL_ADDRESS>
###### Abstract

Many practical engineering systems and their components have multiple
performance levels and failure modes. If these systems form a monotonically
increasing structure function (system model) with respect to the performance
of their components and also if all of their components affect the overall
system performance, then they are said to be multistate coherent systems.
Traditionally, the reliability analysis of these multistate coherent systems
has been carried out using paper-and-pencil or simulation based methods. The
former method is often prone to human errors, while the latter requires high
computational resources for large and complex systems having components with
multiple operational states. As a complimentary approach, we propose to use
Higher-order-logic (HOL) theorem proving to develop a sound reasoning
framework to analyze the reliability of multistate coherent systems in this
paper. This framework allows us to formally verify generic mathematical
properties about multistate coherent systems with an arbitrary number of
components and their states. Particularly, we present the HOL formalization of
series and parallel multistate coherent systems and formally verify their
deterministic and probabilistic properties using the HOL4 theorem prover. For
illustration purposes, we present the formal reliability analysis of the
multistate oil and gas pipeline to demonstrate the effectiveness of our
proposed framework.

###### keywords:

Multistate Coherent Systems, Reliability Analysis, Probabilistic Analysis,
Theorem Proving, Higher-order Logic, HOL4

##  1 Introduction

In many real-life scenarios, engineering systems and their components assume
an entire range of different performance levels or states varying from perfect
functioning to complete failure. Such types of systems are known as multi-
state systems (el1978multistate, ). If a multistate system forms a
monotonically increasing structure function (system model) with respect to the
performance of its components and the overall system performance is dependent
on each one of its component, then it is said to be a multistate coherent
system (el1978multistate, ). The monotonicity property of a multistate
coherent system is described as each system component contributes to the
system performance in a manner that if it fails, then the system performance
also degrades or remains the same but does not improve or vice versa
(ebrahimi1984multistate, ). Similarly, a component is said to be relevant to
the system performance, if it has a direct impact on some performance levels
(ebrahimi1984multistate, ). To analyze the performance of these complex
multistate coherent systems, it is often required to evaluate the reliability
of these systems at all possible performance levels (states) in terms of all
the possible operational states of their components.

Traditionally, simulation based reliability analysis tools, such as ReliaSoft
(coroporation2009reliability, ) and FReET (menvcik2016software, ), have been
used to analyze the reliability of multistate coherent systems. These
simulation tools mainly utilize Monte-Carlo simulation, which is based on
numerical approximation algorithms (billinton1991hybrid, ; zio2007monte, ).
Due to the large number of states involved in analyzing the reliability of
complex multistate coherent systems, these simulation tools are
computationally expensive and can only analyze very small sized systems. In
contrast, the analytical approaches are more scalable than simulation based
methods. For instance, El-Neweihi et al. (el1978multistate, ) developed an
axiomatic theory to analytically analyze the performance of multistate
coherent systems. They described that the performance of multistate coherent
system is lower bounded by the performance of a series system and upper
bounded by a parallel system. They presented several key deterministic and
probabilistic properties, such as system concatenation (redundancy), and
critical upper connection vector bounds, about the multistate coherent
systems. However, the manual approach of using these properties for conducting
the performance analysis of real-world multistate safety-critical systems is
impractical as well as prone to human error since these systems involve a
large number of operational states.

Formal methods (hasan2015formal, ) are computer-based mathematical analysis
techniques that involve constructing a mathematical model based on an
appropriate logic and verification of its various properties based on
deductive reasoning. Higher-order-logic (HOL) theorem proving is a sound
reasoning environment and is widely adopted formal method for performing an
accurate analysis of the engineering systems. It has also been used for
developing a formal dependability analysis framework (ahmad2017formal, ),
based on Reliability Block Diagram (RBD) (trivedi1982probability, ) and Fault
Tree (FT) (trivedi1982probability, ) based modeling techniques, which have
further been used to perform the reliability analysis of oil and gas pipelines
(ahmad2018formal, ) and a railway traction drive system ahmad2019formalization
, failure analysis of satellite solar arrays (ahmad2015towards, ) and an air
traffic management system (ahmad2016formalization, ). However, this framework
(ahmad2017formal, ) is only limited to the binary state systems and cannot be
used to analyze the performance analysis of complex multistate coherent
systems.

In this paper, we propose to use HOL theorem proving, as shown in Figure 1, to
conduct the performance analysis of multistate coherent systems. We
particularly formalize the notion of multistate coherent systems and formally
verify their deterministic and probabilistic properties, such as upper and
lower bounds, system concatenation (redundancy), and critical upper connection
vector bounds. To illustrate the practical effectiveness of our proposed
approach, we conduct the formal performance analysis of the multistate oil and
gas pipeline, which is modeled as a series and parallel multistate coherent
system.

Figure 1: Proposed Framework

The rest of the paper is organized as follows: Section 2 provides a brief
description of various analysis techniques used for performing the
probabilistic performance analysis of systems. We present preliminaries that
include a brief introduction of theorem proving, the HOL4 theorem prover and
the formalization of probability theory in HOL4, in Section 3. Section 4
provides our formalization of multistate coherent systems, i.e., formalization
of the multistate series and parallel structure functions and formal
verification of their deterministic properties. Section 5 presents the
stochastic performance of the multistate coherent systems. We provide the
formal performance analysis of multistate oil and gas pipeline system in
Section 6. Finally, Section 7 concludes the paper.

##  2 Related Work

In this section, we present a brief overview of different analysis techniques
that have been used for the probabilistic performance analysis of the
multistate coherent systems.

###  2.1 Simulation

Many Monte-Carlo based simulation approaches have also been used for assessing
the reliability of multistate coherent systems. For instance, Billinton et al.
(billinton1991hybrid, ) proposed a hybrid approach by combining Monte-Carlo
simulation and an enumeration technique. They also analyzed large scale
composite generation transmission systems by modeling its generation units as
multistate system. Similarly, Zio et al. (zio2007monte, ) proposed a Monte
Carlo simulation based methodology in order to model the complex dynamics of
multi-state components by considering their operational dependencies in the
overall system state. As an extension to their work, they also applied Monte-
Carlo simulation based methodology to evaluate different reliability
importance measures of the components at a given state in a multi-state
series-parallel systems (zio2004estimation, ). Jose et al. (ramirez2005monte,
) presented a Monte-Carlo simulation based approach to evaluate the
reliability of a multistate system. They applied this methodology to a multi-
state system involving two-terminal reliability computation. These simulation
based methodologies pose a limit on their usability in terms of computational
cost when the number of components or their performance levels become large.

###  2.2 Analytical Methods

In the literature, many analytical approaches proposed novel methods to
evaluate the reliability of multi-state systems. A simplest approach among
them is the extension of existing binary models to multi-state cases.
Caldarola (caldarola1980coherent, ) used a Boolean variable to each component
state in a multistate system. This approach also presented a method to reduce
a multistate system to a binary system. Boedidheimer et al.
(boedigheimer1994customer, ) utilized the Binary Decision Diagram (BDD)
approach to determine the reliability of multistate systems. Their methodology
was basically to define a customer-centered structure function that requires
the customers to assign an appropriate number of states for components and the
entire system. Some existing literature also proposed the stochastic process
based analytical methods for reliability evaluation of multistate systems. For
instance, Natvig and Streller (natvig1984steady, ) were the first to introduce
the stochastic process approach for reliability analysis of multistate
systems. Similarly, Aven (aven1999stochastic, ) applied modern theory of
stochastic process to present a more advanced probabilistic framework. This
method greatly facilitated the users to develop general failure models in
order to get formulas for evaluation of various performance measures while
conducting the reliability analysis of multistate systems in complex
situations. Xue et al. (xue1995dynamic, ) presented the idea of combining the
Markov processes and coherent structure function for multistate systems.

El-Neweihi et al. (el1978multistate, ) developed an axiomatic theory to
analytically analyze the performance of multistate coherent systems. This work
utilizes the idea of structure function that describe the relation of system
states to the states of its components. As compared to other analytical
approaches in this domain, their work is simplistic and systematic
representation of the multistate coherent systems and their deterministic and
probabilistic properties.

All these analytical approaches are carried out manually using paper-and-
pencil based methods and thus are prone to human errors when the system is
large and complex.

###  2.3 Proposed Approach

Recently, a formal dependability analysis framework (ahmad2017formal, ), based
on Reliability Block Diagram (RBD) (trivedi1982probability, ) and Fault Tree
(FT) (trivedi1982probability, ) modeling techniques, has been developed using
HOL theorem prover. This framework has been successfully utilized to carry out
the reliability analysis of oil and gas pipelines (ahmad2018formal, ) and a
railway traction drive system (ahmad2019formalization, ), failure analysis of
satellite solar arrays (ahmad2015towards, ) and an air traffic management
system (ahmad2016formalization, ). Ahmad et al. (ahmad2019formalization, )
also presented the formalization of reliability importance measures and
analyzed a railway signaling system. However, this framework (ahmad2017formal,
) is only limited to the binary state systems and cannot be used to analyze
the performance analysis of complex multistate coherent systems. In this work,
we formalize from scratch, the notion of multistate coherent systems and their
probabilistic analysis using HOL theorem proving. The main idea is to analyze
the performance of multistate coherent systems by considering the performance
states of each of their components. We particularly formalize the work of El-
Neweihi et al. (el1978multistate, ), to build the formal reasoning support to
conduct the reliability analysis of multistate coherent series and parallel
systems. We also present the HOL formalization of their deterministic and
probabilistic properties essentially required to analyze the system
performance. To the best of our knowledge, this is the first formal work
describing the formalization of the multistate coherent system using HOL
theorem proving.

##  3 Preliminaries

This section presents a brief introduction to theorem proving, the HOL4
theorem prover and the formalization of probability theory in the HOL4 theorem
prover to facilitate the understanding of the rest of the paper.

###  3.1 Theorem Proving

Theorem proving (gordon_89, ) is a broadly used formal verification technique.
The system that we wish to analyze is first mathematically modeled in an
appropriate logic and then its properties of interest are verified using
computer-based formal tools. The use of formal logics as a modeling approach
makes theorem proving a very adaptable verification tool as it is feasible to
formally verify any system that can be presented mathematically. The core of
theorem provers typically consists of some universal axioms and primitive
inference rules. Soundness is guaranteed as each new theorem should be created
from these fundamental or already proved theorems and primitive inference
rules. The verification effort of a theorem in a theorem prover varies from
trivial to complicated, relying on the underlying logic (harrison_96a, ).

###  3.2 HOL4 Theorem Prover

HOL4 (gordon1993introduction, ) is an interactive theorem prover that was
developed at the University of Cambridge, UK for proving theorems in higher-
order logic. This makes use of the simple type theory of Church (church_40, )
along with Hindley-Milner polymorphism (milner_77, ) to implement higher-order
logic. It has been successfully employed as a verification methodology for
both software and hardware as well as a platform for the formalization of pure
mathematics. The HOL4 core consists of only $4$ basic axioms and $8$ primitive
inference rules, which are implemented as Meta Language (ML paulson1996ml , a
general-purpose functional programming language) 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 work, we utilize the HOL4 theories of
Boolean, lists, sets, positive integers, _real_ numbers, measure and
probability (mhamdi_11, ). In fact, one of the primary motivations of
selecting the HOL4 theorem prover for our work was to benefit from these
built-in mathematical theories. Table 1 provides the mathematical
interpretations of some frequently used HOL4 symbols and functions, which are
inherited from existing HOL4 theories.

HOL4 Symbols | Standard Symbols | Meaning
---|---|---
/\ | and | Logical and
\/ | or | Logical or
$\neg$ | not | Logical negation
$\mathtt{::}$ | $cons$ | Adds a new element to a list
$\mathtt{MEM\ a\ L}$ | $member$ | True if $a$ is a member of list $L$
LENGTH L | length | Length of list L
(a,b) | a $\times$ b | A pair of two elements
FST | fst(a,b) = a | First component of a pair
SND | snd(a,b) = b | Second component of a pair
$\lambda$x.t |  $\lambda$x.t | Function that maps x to t(x)
{x|P(x)} | $\\{\lambda x.P(x)\\}$ | Set of all x such that P(x)
SUC n | (n + 1) | Successor of natural number
Table 1: HOL4 Symbols and Functions

###  3.3 Probability Theory

In mathematics, a measure space is described as a triple
$(\Omega,\Sigma,\mu)$, where $\Omega$ is a sample space set, $\Sigma$ denotes
a $\sigma$-algebra of subsets of $\Omega$, where the subsets are usually known
as measurable sets, and $\mu$ is a measure on domain $\Sigma$. A probability
space defined on a measure space $(\Omega,\Sigma,Pr)$, such that the measure,
denoted by $Pr$, is called the probability with the measure of sample space
$\Omega$ equal to $1$, i.e., $Pr(\Omega)=1$. In the HOL4 formalization of
probability theory mhamdi_11 , given a probability space $p$, the functions
space, subsets and prob return the corresponding $\Omega$, $\Sigma$ and $Pr$,
respectively. Probability theory in HOL4 provides many basic probability
axioms which have been formally verified, that play an important role in
formal reasoning about probabilistic properties of multi-state coherent
systems. Random variable is the function defined on sample space. It takes all
the possible outcome of sample space and maps them to mathematically easier
outcome labels, usually a real number.

##  4 Multistate Coherent Systems

To facilitate the reader understanding, we first present the basic notations
and the terminologies related to the mathematical representation of multistate
systems. The notation $\mathbf{x}=(x_{1},\cdots,x_{n})$ denotes the state
vector representing the operational states of components $1,\cdots,n$.
$S=\\{0,1,\cdots,M\\}$ represents the set of operational states that a system
and its component can acquire as performance levels.

  * •

$(j_{i},\mathbf{x})\equiv(x_{1},\cdots,x_{i-1},j,x_{i+1},\cdots,x_{n})$, where
$j=0,1,\cdots,M$, describes that value $j$ is substituted at $i^{th}$ index of
vector $\mathbf{x}$.

  * •

$(\mathbf{\cdot}_{i},\mathbf{x})\equiv(x_{1},\cdots,x_{i-1},\mathbf{\cdot},x_{i+1},\cdots,x_{n})$,
where $\cdot$ describes that an arbitrary value is substituted at $i^{th}$
index of vector $\mathbf{x}$.

  * •

$\mathbf{j}\equiv(j,j,\cdots,j)$ is a state vector $\mathbf{j}$ with all
values equal to $j$.

  * •

$\mathbf{y}\wedge\mathbf{x}\equiv(y_{1}\wedge x_{1},\cdots,y_{n}\wedge
x_{n})$, where $y\wedge x=min(y,x)$, defines the relationship between the
corresponding elements of two equal length vectors returning a vector with
entries of the minimum value of the corresponding elements. The relation
$y\wedge x=min(y,x)$ can be viewed as the components $x$ and $y$ that are
connected in series.

  * •

$\mathbf{y}\vee\mathbf{x}\equiv(y_{1}\vee x_{1},\cdots,y_{n}\vee x_{n})$,
where $y\vee x=max(y,x)$, returns a vector with entries of the maximum value
of the corresponding elements. The relation $y\vee x=max(y,x)$ can be viewed
as the components $x$ and $y$ that are connected in parallel.

  * •

$\mathbf{y}<\mathbf{x}$, where $y_{i}\leq x_{i}$ for $i=1,\dots,n$, and
$y_{i}<x_{i}$ for some $i$, ensures that all the elements (components states)
in $\mathbf{y}$ are less than or equal to the corresponding elements in
$\mathbf{x}$ or at least one element in $\mathbf{y}$ is less than the
corresponding element in $\mathbf{x}$.

  * •

Describing $f(x_{1},\cdots,x_{n})$ as an increasing function states that $f$
is increasing in each of its argument.

  * •

Given a distribution function $F$, the notation $\overline{F}$ represents its
complement $1-F$ in the probability space.

Consider a system having $n$ components while both the system and its
components can assume a set of distinct finite states depicting different
levels of performance varying from perfect functioning mode (State $M$) to
complete failure mode (State $0$). As the time of operation increases, the
component performance, given it was working in perfect functioning state $M$
initially, degrades and enters a State $M-1$, and upon further degradation it
enters the state $M-2$. Finally, the component reaches the State $0$, whereas
an identical sequence of decreasing state levels illustrates the working of
system over time.

The vector $\mathbf{x}=(x_{1},x_{2},\ldots,x_{i},\ldots,x_{n})$ represents a
state vector with $n$ components, where the performance level $x_{i}$ of
component $i$ presumes a value in the set $S=\\{0,1,\cdots,M\\}$. In this
work, we consider that the performance of the system is completely determined
by the performance of its components. Thus, the state of the system is related
to the states of its components by a function
$\phi(\mathbf{x}):S^{n}\rightarrow S$. In other words, if we know the state
vector $\mathbf{x}$, then we can obtain the value of $\phi(\mathbf{x})$
representing the system state. The function $\phi(\mathbf{x})$ is also known
as the structure function of the system.

According to El-Neweihi et al. el1978multistate , a multistate system
qualifies to be coherent if its structure function, $\phi(\mathbf{x})$, meets
the following conditions:

  1. (1)

$\phi(\mathbf{x})$ is increasing.

  2. (2)

For level $j$ of component $i$, there exists a vector
$(\mathbf{\cdot}_{i},\mathbf{x})$ such that $\phi({j}_{i},\mathbf{x})=j$ while
$\phi({l}_{i},\mathbf{x})\neq j$ for $l\neq j$, $i=1,\cdots,n$, and
$j=0,1,\cdots,M$.

  3. (3)

$\phi(\mathbf{j})=j$ where $j=0,1,\ldots,M$.

Condition ($1$) is the monotonicity of the system structure function, which
states that if a system component improves its performance, then the system
performance may improve or remain unchanged but does not degrade, or vice
versa. Similarly, Condition ($2$) states that each component is _relevant_ to
the system performance at all of its operational states. Condition ($3$)
follows from the above two conditions and describes that if all the components
are in the same operational state, say $j$, then the system will also be
operating in that state $j$. Some basic types of multistate coherent systems
are as follows:

  1. (1)

A series system: $\phi_{series}(\mathbf{x})=\min\limits_{i=1}^{n}x_{i}$.

  2. (2)

A parallel system: $\phi_{parallel}(\mathbf{x})=\max\limits_{i=1}^{n}x_{i}$.

  3. (3)

A $k$-out-of-$n$ structure: $\phi_{k-\mathrm{out-
of}-n}(\mathbf{x})=x_{(n-k+1)}$, where $x_{(1)}\leq x_{(2)}\leq\cdots\leq
x_{(n-1)}\leq x_{(n)}$ is an ascending rearrangement of
$x_{1},x_{2},\cdots,x_{n-1},x_{n}$.

In the next sections, we present the HOL formalization of series and parallel
multistate coherent systems. We formally verify that they satisfy the
essential conditions of multistate coherent systems and also their respective
deterministic properties, such as upper and lower bounds, redundancy, and
bounds related to the upper critical connection vector.

###  4.1 Multistate Series Structure Function ($\phi_{series}$)

A series system can be mathematically expressed as
$\phi_{series}(\mathbf{x})=\min\limits_{i=1}^{n}x_{i}$. We can formally define
it in HOL4 as follows:

######  Definition 4.1.

_Multistate Series Structure Function_
$\vdash_{def}$ (series_MS [] = (0:num)) $\wedge$
($\forall$x. series_MS [x] = (x:num)) $\wedge$
($\forall$x xs. series_MS ((x:num)::xs) = MIN x (series_MS xs))

The above function takes the states of the components as a list and returns
the minimum state by recursively applying the HOL4 minimum function MIN. Using
Definition 4.1, we can formally verify that $\phi_{series}$ satisfies the
multistate coherent systems Conditions ($1$-$3$) as:

######  Theorem 4.1.

_Multistate Coherent Systems Condition $1$ for $\phi_{series}$_
$\vdash_{thm}$ $\forall$(L:(num#num) list).
[A1:] $\neg$NULL L $\wedge$
[A2:] X_LOW_Y (X_list L) (Y_list L)
$\Rightarrow$ (series_MS (X_list L) $\leq$ series_MS (Y_list L))

The above theorem satisfies the monotonicity property (Condition ($1$)) for
the series structure function $\phi_{series}(\mathbf{x})$. Assumption A1
states that the components state vectors must not be empty. The functions
X_list and Y_list are defined in HOL4 to extract the component state vectors
from a list of pairs, where the first element of the pair are the elements of
state vector X and the second element of the pair belongs to the state vector
Y, respectively. For example, X_list [(x1,y1),(x2,y2)] = [x1;x2]. The function
X_LOW_Y in Assumption A2 formally defines the relationship
$\mathbf{x}<\mathbf{y}$ explained above and is formalized in HOL4 as:

######  Definition 4.2.

_Components States in $\mathbf{x}$ are less than Elements in $\mathbf{y}$_
$\vdash_{def}$ (X_LOW_Y [] = T) $\wedge$
($\forall$h t. X_LOW_Y (h::t) =
(FST h $\leq$ SND h) $\wedge$ X_LOW_Y t)

where the HOL4 functions FST and SND accept a pair and return the first and
second element of the pair, respectively. The verification of Theorem 4.1 is
mainly based on induction, Definitions 4.1 and 4.2 alongwith some arithmetic
reasoning.

######  Theorem 4.2.

_Multistate Coherent Systems Condition $2$ for $\phi_{series}$_
$\vdash_{thm}$ $\forall$l j L i.
[A1:] l$\ \neq$ j $\wedge$
[A2:] i < LENGTH L $\wedge$
[A3:] $\neg$NULL L $\wedge$
[A4:] ($\forall$x. MEM x L $\Rightarrow$ x > j) $\wedge$
[A5:] (series_MS (LUPDATE j i L) = j)
$\Rightarrow$ (series_MS (LUPDATE l i L) $\neq$ j)

Assumption A1 makes sure that l must not equal to j. Assumption A2 ensures
that the value of index i must not exceed the length of the list L. Assumption
A3 is same as Assumption A1 of Theorem 4.1. Assumption A4 guarantees that all
the elements in the components state vector L must be greater than State j.
Assumption A5 ensures that the system acquires the State j only when the
component i in the state vector L is updated to the state value j as all other
components are in the state greater than j. The HOL4 function LUPDATE in above
theorem models the notation $(j_{i},\mathbf{x})$, i.e., it updates the
$i^{th}$ element of vector $\mathbf{x}$ with value j. Theorem 4.2 satisfies
the component relevancy property (Condition ($2$)) for the series structure
function $\phi_{series}(\mathbf{x})$. The proof process of Theorem 4.2 is
based on induction and Definition 4.1 alongwith some properties of lists.

######  Theorem 4.3.

_Multistate Coherent Systems Condition $3$ for $\phi_{series}$_
$\vdash_{thm}$ $\forall$L j.
[A1:] $\neg$NULL L $\wedge$
[A2:] ($\forall$x. MEM x L $\Rightarrow$ x = j)
$\Rightarrow$ (series_MS L = j)

where Assumption A1 in the above theorem is same as Assumption A1 of Theorem
4.1. Assumption A2 ensures that all the components must be in State j. This
implies that the multistate series structure function $\phi_{series}$ will
also be in State j (Condition ($3$)). The verification of Theorem 4.3 is based
on Definition 4.1 and properties of lists alongwith arithmetic reasoning. From
Theorems 4.1\- 4.3, we can conclude that the $\phi_{series}$ is a multistate
coherent structure function.

###  4.2 Deterministic Properties for $\phi_{series}$

We now present the HOL formalization of the deterministic properties for
$\phi_{series}$, such as upper and lower bounds, system concatenation, and
critical upper connection vector bounds, as follows:

######  Theorem 4.4.

_Lower and Upper Bounds for $\phi_{series}$_
$\vdash_{thm}$ $\forall$X. min_vec X $\leq$ series_MS X $\wedge$
series_MS X $\leq$ max_vec X

The functions min_vec and max_vec take the components state vector X in the
form of a list and return the minimum and maximum states, respectively. The
above theorem verifies the lower and upper bounds for $\phi_{series}$.

The property
$\phi_{series}(\mathbf{x}\vee\mathbf{y})\geq\phi_{series}(\mathbf{x})\vee\phi_{series}(\mathbf{y})$
describes the effect of redundancy at the component and system levels for
$\phi_{series}$ where the left hand side of the inequality represents the
redundancy at the component level and the right hand side gives the redundancy
at the system level. We formally verify this inequality in HOL4 as follows:

######  Theorem 4.5.

_Relationship of Redundancy at the Component and System levels_
$\vdash_{thm}$ $\forall$L. series_MS (X_OR_Y L) $\geq$
MAX (series_MS (X_list L)) (series_MS (Y_list L))

The function X_OR_Y models the notation $\mathbf{x}\vee\mathbf{y}$ where the
functions X_list and Y_list represent the state vectors $\mathbf{x}$ and
$\mathbf{y}$, respectively. The function X_OR_Y is formally modeled in HOL4 as
follows:

######  Definition 4.3.

_Function $\mathbf{x}\vee\mathbf{y}$_
$\vdash_{def}$ (X_OR_Y [] = []) $\wedge$
$(\forall$h t. X_OR_Y (h::t) =
(MAX (FST h) (SND h))::(X_OR_Y t))

Similarly, the property
$\phi_{series}(\mathbf{x}\wedge\mathbf{y})=\phi_{series}(\mathbf{x})\wedge\phi_{series}(\mathbf{y})$
describes that $\phi_{series}$ is compositional in nature, i.e., a system
level structure function is composed of component level structure functions.
We formally verify this relationship in HOL4 as:

######  Theorem 4.6.

_Compositional Nature of $\phi_{series}$_
$\vdash_{thm}$ $\forall$L. series_MS (X_AND_Y L) =
MIN (series_MS (X_list L))
(series_MS (Y_list L))

The function X_AND_Y models the notation $\mathbf{x}\wedge\mathbf{y}$ and it
is formally defined in HOL4 as follows:

######  Definition 4.4.

_Function $\mathbf{x}\wedge\mathbf{y}$_
$\vdash_{def}$ (X_AND_Y [] = []) $\wedge$
$(\forall$h t. X_AND_Y (h::t) =
(MIN (FST h) (SND h))::(X_AND_Y t))

The concept of bounds on $\phi_{series}(\mathbf{x})$ is realized by special
kinds of component state vectors, namely $connection$ $vectors$ and $upper$
$critical$ $connection$ $vectors$. They are especially quite useful when the
entire system performance is difficult to evaluate and one wants to know the
bounds of system performance relative to some known state vectors. We formally
define these concepts in HOL4 as follows:

######  Definition 4.5.

_A vector $\mathbf{x}$ is defined to be a connection vector to level $j$ if
$\phi(\mathbf{x})=j$, $j=0,1,\cdots,M$._
$\vdash_{def}$ $\forall$X j $\mathtt{\phi}$. con_vec X j $\mathtt{\phi}$ =
(($\mathtt{\phi}$ X) = (j:num))

######  Definition 4.6.

_A vector $\mathbf{x}$ is defined to be an upper critical connection vector to
level j if $\phi(\mathbf{x})=j$ and strictly $\mathbf{y}$ $<$ $\mathbf{x}$
implies $\phi(\mathbf{x})<j$, $j=0,1,\cdots,M$._
$\vdash_{def}$ $\forall$X j $\phi$. uc_con_vec X j $\phi$ =
con_vec X j $\phi$ $\wedge$
($\forall$Y. (X_LOWER_Y ZIP (Y,X)) $\Rightarrow$ $\phi$ Y < j)

where the HOL4 function ZIP converts a pair of lists
$([x_{1},...,x_{n}],[y_{1},...,y_{n}])$ to a list of pairs
$[(x_{1},y_{1}),...,(x_{n},y_{n})]$. The function X_LOWER_Y models the strict
case of the notation $\mathbf{y}<\mathbf{x}$ similar to the non-strict case of
the notation defined by the function X_LOW_Y (Definition 4.2).

######  Definition 4.7.

_Set of Upper Critical Connection Vectors to Level $j$_
$\vdash_{def}$ ($\forall$Y $\phi$ j. uc_con_vec_set0 (0:num)
Y j $\phi$ = uc_con_vec (Y 0) j $\phi$) $\wedge$
($\forall$Y $\phi$ j n. uc_con_vec_set0
(SUC n) Y j $\phi$ =
uc_con_vec (Y (SUC n)) j $\phi$ $\wedge$
uc_con_vec_set0 n Y j $\phi$)

######  Theorem 4.7.

_System is Lower Bounded by Level $j$_
$\vdash_{thm}$ $\forall$n Y j l X.
[A1:] $\neg$NULL (X) $\wedge$
[A2:] n $\geq$ l $\wedge$
[A3:] LENGTH (Y l) = LENGTH X $\wedge$
[A4:] X_LOW_Y (Y l) X $\wedge$
[A5:] uc_con_vec_set0 n Y j series_MS
$\Rightarrow$ (series_MS X $\geq$ j)

The above property states that if an upper critical vector of a system to
level j is known, then the system will be lower bounded by level j for all
those state vectors that are upper vectors to the system’s upper critical
vector.

###  4.3 Multistate Parallel Structure Function ($\phi_{parallel}$)

A parallel system can be expressed mathematically as
$\phi_{parallel}(\mathbf{x})=\max\limits_{i=1}^{n}x_{i}$.

######  Definition 4.8.

_Multistate Parallel Structure Function_
$\vdash_{def}$ (parallel_MS [] = (0:num)) $\wedge$
($\forall$x. parallel_MS [x] = x:num) $\wedge$
($\forall$x xs. parallel_MS ((x:num)::xs) =
MAX x (parallel_MS xs))

The above function is defined similar to Definition 4.1 except the function
MAX is used to model the multistate parallel system. We formally verify
Condition $1$ of multistate coherent systems for $\phi_{parallel}$ as the
following HOL4 theorem:

######  Theorem 4.8.

_Multistate Coherent Systems Condition $1$ for $\phi_{parallel}$_
$\vdash_{thm}$ $\forall$(L:(num#num) list).
[A1:] $\neg$NULL L $\wedge$
[A2:] X_LOW_Y (X_list L) (Y_list L)
$\Rightarrow$ (parallel_MS (X_list L) $\leq$
parallel_MS (Y_list L))

Assumptions A1-A2 are the same as that of Theorem 4.1. The proof process of
Theorem 4.8 is mainly based on induction and Definition 4.8 alongwith some
arithmetic reasoning. Similarly, we formally verify Condition $2$ for
$\phi_{parallel}$ as:

######  Theorem 4.9.

_Multistate Coherent Systems Condition $2$ for $\phi_{parallel}$_
$\vdash_{thm}$ $\forall$l j L i.
[A1:] l$\ \neq$ j $\wedge$
[A2:] i < LENGTH L $\wedge$
[A3:] $\neg$NULL L $\wedge$
[A4:] ($\forall$x. MEM x L $\Rightarrow$ x > j) $\wedge$
[A5:] (parallel_MS (LUPDATE j i L) = j)
$\Rightarrow$ (parallel_MS (LUPDATE l i L) $\neq$ j)

Assumptions A1-A4 are the same as that of Theorem 4.2. Assumption A5 ensures
that the system acquires the State j only when the component i in the state
vector L is updated to the state value j as all other components are in the
state greater than j. The verification of Theorem 4.9 is mainly based on
induction, Definition 4.8 alongwith some properties of lists.

######  Theorem 4.10.

_Multistate Coherent Systems Condition $3$ for $\phi_{parallel}$_
$\vdash_{thm}$ $\forall$L j.
[A1:] $\neg$NULL L $\wedge$
[A2:] ($\forall$x. MEM x L $\Rightarrow$ x = j)
$\Rightarrow$ (parallel_MS L = j)

Assumptions A1-A2 are the same as that of Theorem 4.3. The proof process of
Theorem 4.10 is mainly based on induction, Definition 4.8 and properties of
lists alongwith some arithmetic reasoning.

###  4.4 Deterministic Properties of $\phi_{parallel}$

Similar to Section 4.2, we formally verify the deterministic properties for
$\phi_{parallel}$ as follows:

######  Theorem 4.11.

_Lower and Upper Bounds for $\phi_{parallel}$_
$\vdash_{thm}$ $\forall$X. min_vec X $\leq$ parallel_MS X $\wedge$
parallel_MS X $\leq$ max_vec X

######  Theorem 4.12.

_Relationship of Redundancy at the Component and System levels_
$\vdash_{thm}$ $\forall$L. parallel_MS (X_OR_Y L) =
MAX (parallel_MS (X_list L))
(parallel_MS (Y_list L))

It is worth mentioning that the redundancy for $\phi_{parallel}$ at the
component level has same effect as the redundancy at the system level which is
opposite to the result of Theorem 4.12 for $\phi_{series}$, where the
component level redundancy surpasses the system level redundancy.

######  Theorem 4.13.

_Compositional Nature of $\phi_{parallel}$_
$\vdash_{thm}$ $\forall$L. parallel_MS (X_AND_Y L) $\leq$
MIN (parallel_MS (X_list L)) (parallel_MS (Y_list L))

Similarly, Theorem 4.13 shows that the sequential concatenation at the
component level is worse than the sequential concatenation at the system level
for $\phi_{parallel}$. This result is also in contrast to Theorem 4.6, which
describes that sequential concatenation at the component level has same effect
as the sequential concatenation at the system level for $\phi_{series}$.

Similarly, following theorem verifies the bound on $\phi_{parallel}$ described
by the upper critical connection vector, similar to the result of Theorem 4.7
for $\phi_{series}$.

######  Theorem 4.14.

_System is Lower Bounded by Level $j$_
$\vdash_{thm}$ $\forall$n Y j l X.
[A1:] $\neg$NULL (X) $\wedge$
[A2:] n $\geq$ l $\wedge$
[A3:] LENGTH (Y l) = LENGTH X $\wedge$
[A4:] X_LOW_Y (Y l) X $\wedge$
[A5:] uc_con_vec_set0 n Y j
parallel_MS
$\Rightarrow$ (parallel_MS X $\geq$ j)

##  5 Stochastic performance of multistate coherent systems

In this section, we formalize the relationship between the probabilistic
performance of of multistate coherent systems and their components. Let
$X_{i}$ be the random state of $i^{th}$ component, with

$P[X_{i}=j]=p_{ij},$ (1)

$P[X_{i}\leq j]=P_{i}(j),$ (2)

where $P_{i}$ be the $performance$ $distribution$ of $i^{th}$ component and
$j=0,1,\cdots,M$ and $i=1,2,\cdots,n$.

$P_{i}(j)=\sum_{k=0}^{j}p_{ik},$ (3)

$P_{i}(M)=\sum_{k=0}^{M}p_{ik}=1.$ (4)

In order to formalize the above equations, we first formally define the events
for probability mass and distribution functions in HOL4 as:

######  Definition 5.1.

_Event for Probability Mass Function_
$\vdash_{def}$ $\forall$X p j.
PMF_random_state_event X p j =
{x | (X x) = (j:num)} $\cap$ p_space p

######  Definition 5.2.

_Event for Probability Distribution Function_
$\vdash_{def}$ $\forall$X p j.
CDF_rand_state_event X p j =
{x | (X x) $\leq$ (j:num)} $\cap$ p_space p

The function PMF_random_state_event describes the event when a component is
acquiring an arbitrary State j. Similarly, the function CDF_rand_state_event
models the event for cumulative distribution function (CDF) describing the
event when a component is acquiring a state value equal to or less than an
arbitrary state value j. Now, the PMF of a random component state can be
modeled in HOL4 as follows:

######  Definition 5.3.

_PMF of a Random Component State_
$\vdash_{def}$ $\forall$X p j. PMF_component X p j =
prob p (PMF_random_state_event X p j)

where X is the random state variable, p represents the probability space and j
represents a state value. The HOL4 function prob takes the probability space
and an event within the probability space, and returns the probability of the
event

The CDF of the random state variable can be modeled in HOL4 as follows:

######  Definition 5.4.

_CDF of the Random State Variable_
$\vdash_{def}$ $\forall$X p j. CDF_component X p j =
prob p (CDF_rand_stat_event X p j)

Using Definitions 5.3 and 5.4, we can also verify that the performance
distribution of a random state variable is equal to sum of its performances of
corresponding states as described in Equation (3).

######  Theorem 5.1.

_Performance Distribution of a Random State Variable_
$\vdash_{thm}$ $\forall$X p j.
[A1:] prob_space p $\wedge$
[A2:] ($\forall$l. PMF_random_state_event X
p l $\in$ events p)
$\Rightarrow$ (CDF_component X p j =
$\sum\limits_{k=0}^{j}$ PMF_component X p k)

Similarly, we formally prove the important property of the performance
distribution of component random state variable as described in Equation (4),
as follows:

######  Theorem 5.2.

_Performance Distribution of Component Random State Variable_
$\vdash_{thm}$ $\forall$X p M.
[A1:] prob_space p $\wedge$
[A2:] component_events_space X M =
p_space p
$\Rightarrow$ CDF_component X p M = 1

where Assumption A1 ensures that p is a valid probability space. Assumption A2
asserts that the component state variable has the maximum state value M and
all the events, defined by the states of the component, form a valid sample
space in p. The function component_events_space takes a random component state
variable X and its maximum state value M, and returns the union of all the
events representing the sample space of X. This function is formally defined
in HOL4 as follows:

######  Definition 5.5.

_Union of all Events Representing the Sample Space of X_
$\vdash_{def}$ ($\forall$X. component_events_space X 0 =
PREIMAGE X 0) $\wedge$
($\forall$X M. component_events_space X
(SUC M) =
component_events_space X M $\cup$
PREIMAGE X {SUC M})

###  5.1 System Level Performance

Now, we describe the system level probabilities in HOL4. Let
$\mathbf{X}=(X_{1},\cdots,X_{n})$ be the random vector depicting the random
state variables of the components $1,\cdots,n$, where the $X_{1},\cdots,X_{n}$
are taken as statistically mutually independent in nature. Then,
$\phi(\mathbf{X})$ is the random variable that describes the random state of
the multistate coherent system having structure function $\phi(\mathbf{x})$,
with

$P[\phi(\mathbf{X})=j]=p_{j},\ \ \ \ \ j=0,1,\cdots,M.$ (5)

$P[\phi(\mathbf{X})\leq j]=P(j),\ \ \ \ j=0,1,\cdots,M.$ (6)

where $P$ denotes the performance distribution of the system. We formalize the
above equations in HOL4 as follows:

######  Definition 5.6.

_PMF of $\phi$ State Event_
$\vdash_{def}$ $\forall$X $\phi$ p j. PMF_PHI_state_event
($\phi$:num list -> num) X p j =
{x | $\phi$ (MAP ($\lambda$a. a x) X) = (j:num)} $\cap$
p_space p

######  Definition 5.7.

_CDF of $\phi$ State Event_
$\vdash_{def}$ $\forall$X $\phi$ p j. CDF_PHI_state_event
($\phi$:num list -> num) X p j =
{x | $\phi$ (MAP ($\lambda$a. a x) X) $\leq$ (j:num)} $\cap$
p_space p

######  Definition 5.8.

_PMF of $\phi$_
$\vdash_{def}$ $\forall$X $\phi$ X p j. PMF_PHI $\phi$ X p j =
prob p (PMF_PHI_state_event $\phi$ X p j)

######  Definition 5.9.

_CDF of $\phi$_
$\vdash_{def}$ $\forall$X $\phi$ X p j. CDF_PHI $\phi$ X p j =
prob p (CDF_PHI_state_event $\phi$ X p j)

Now, we formalize the probabilistic properties of the system performance, such
as its dependency on the performance of its components and its upper and lower
bounds in terms of its components performances. We have formally proved these
properties for both $\phi_{series}$ and $\phi_{parallel}$ structure functions.
If a lower performance component is replaced with a higher performance
component, then the system performance must be improved for coherent systems.
We formally verify this property in HOL4 as:

######  Theorem 5.3.

_Let $P_{i}$, $P_{i}^{{}^{\prime}}$ be two possible performance distributions,
i = 1, $\cdots$, n. Further assume $P_{i}(j)\geq P_{i}^{{}^{\prime}}(j)$ for j
= 0, 1, $\cdots$, M and i=1, $\cdots$, n. Let P and $P^{{}^{\prime}}$ be the
corresponding system performance distributions. Then $P(j)\geq
P^{{}^{\prime}}(j)$ for j = 0, 1, $\cdots$, M._
$\vdash_{thm}$ $\forall$L j p.
[A1:] $\neg$NULL L $\wedge$
[A2:] prob_space p $\wedge$
[A3:] $\forall$l. MEM l L
$\Rightarrow$ CDF_rand_stat_event (FST l)
p j $\in$ events p $\wedge$
[A4:] $\forall$l. MEM l L
$\Rightarrow$ CDF_rand_stat_event (SND l)
p j $\in$ events p $\wedge$
[A5:] $\forall$l. MEM l L
$\Rightarrow$ CDF_rand_stat_event (FST l) p
j $\subset$ CDF_rand_stat_event (SND l) p j
$\Rightarrow$ (CDF_PHI series_MS (X_list L) p j $\leq$
CDF_PHI series_MS (Y_list L) p j $\wedge$
CDF_PHI parallel_MS (X_list L) p j $\leq$
CDF_PHI parallel_MS (Y_list L) p j)

Assumptions A1 and A2 are same as Assumptions A1 of Theorems 4.1 and 5.2.
Assumptions A3 and A4 ensure that all the events associated with the component
states must belong to the event space p. Assumption A5 ensures the condition
$P_{i}^{{}^{\prime}}(j)\leq P_{i}(j)$.

The next property describes the lower bound on the system performance
distribution and is formally verified in HOL4 as:

######  Theorem 5.4.

_Let $P_{i}$, be the performance distribution of component i, for i= 1,
$\cdots$, n and all the components are mutually independent. Then, for j = 0,
1, $\cdots$, M-1 : $\prod_{i=1}^{n}P_{i}(j)\leq P(j)$._
$\vdash_{thm}$ $\forall$L j p.
[A1:] $\neg$NULL L $\wedge$
[A2:] prob_space p $\wedge$
[A3:] ($\forall$l. MEM l L
$\Rightarrow$ (CDF_rand_stat_event l p
j $\in$ events p)) $\wedge$
[A4:] (mutual_indep p (MAP
($\lambda$a. CDF_rand_stat_event a p j) L))
$\Rightarrow$ (list_prod (MAP
($\lambda$a. CDF_component a p j) L) $\leq$
CDF_PHI series_MS L p j)

Similarly, we can formally verify the above property for multistate parallel
coherent system as follows:

######  Theorem 5.5.

_Theorem 5.4 for Multistate Parallel Coherent Systems_
$\vdash_{thm}$ $\forall$L j p.
[A1:] $\neg$NULL L $\wedge$
[A2:] prob_space p $\wedge$
[A3:] ($\forall$l. MEM l L
$\Rightarrow$ (CDF_rand_stat_event l p
j $\in$ events p)) $\wedge$
[A4:] (mutual_indep p (MAP
($\lambda$a. CDF_rand_stat_event a p j) L))
$\Rightarrow$ (list_prod (MAP
($\lambda$a. CDF_component a p j) L) $\leq$
CDF_PHI parallel_MS L p j)

The function mutual_indep adapted from Ahmad et al.’s work ahmad2015towards ,
defines the mutual independence of the events given in the list. Similarly,
the function list_prod returns the product of all the elements in the given
list.

Similarly, the upper bound on the system performance distribution can be
formally verified as follows:

######  Theorem 5.6.

_Let $P_{i}$, be the $i^{th}$ component performance distribution for i= 1,
$\cdots$, n and the components are mutually independent. Then, for j = 0, 1,
$\cdots$, M-1: $P(j)\leq 1-\prod_{i=1}^{n}\overline{P}_{i}(j)$._
$\vdash_{thm}$ $\forall$L j p.
[A1:] $\neg$NULL L $\wedge$
[A2:] prob_space p $\wedge$
[A3:] ($\forall$l. MEM l L
$\Rightarrow$ (CDF_rand_stat_event l p
j $\in$ events p)) $\wedge$
[A4:] (mutual_indep p (MAP
($\lambda$a. CDF_rand_stat_event a p j) L))
$\Rightarrow$ (CDF_PHI series_MS L p j $\leq$
1 - list_prod (MAP
($\lambda$a. compl_CDF_component a p j) L))

where the function compl_CDF_component is the compliment function of the
function CDF_component, depicting the notations $\overline{P}_{i}(j)$ and
${P}_{i}(j)$, respectively. This function is formally defined in HOL4 as
follows:

######  Definition 5.10.

_Compliment Function of CDF_component_
$\vdash_{def}$ $\forall$ $\phi$ X p.
compl_CDF_component X p =
$\lambda$a. (1 - CDF_component X p a)

Figure 2 provides an illustration of the execution of the formal proof of
Theorem 5.6 in HOL$4$

Figure 2: Execution of the Formal Proof of Theorem 5.6

##  6 Performance Analysis of Multistate Oil and Gas Pipeline System

The performance analysis of the oil and gas pipelines is necessary to get
insights about their life and usability. A typical long-distance oil and gas
pipeline can be partitioned into a series connection of $N$ segments, where
these segments may be in different operational states based on their
individual failure times. The working levels of the pipeline and its segments
can acquire any level in $0,\ 1,\ \cdots,\ M$, where $0$ represents the
complete failure state and $M$ denotes the perfect working state. For example,
a $60$ segment pipeline is analyzed in Zhang et al.’s work
zhang2008reliability  using the concept of segments but this work considers
only two states of operation for each segment. In the following sections, we
present the formal performance analysis of a multistate coherent series oil
and gas pipeline, as depicted in Figure 3. This formal analysis is a two step
process. In the first step, we need to formally specify the pipeline segment,
which mainly includes the formal modeling of the pipeline segments and their
different states probabilities. In the next step, these formal models are used
for formally verifying the performance distribution of the series oil and gas
pipeline operating in different states.

Figure 3: An Oil and Gas Pipeline Depicting $10$ Segments

###  6.1 Formal Specifications

A pipeline segment can be completely specified with its operational states and
corresponding state probabilities. We can formally define the segment by
specifying its random state variable and the state probabilities as follows:

######  Definition 6.1.

_Segment State Probability_
$\vdash_{def}$ $\forall$p s. CDF_seg p s =
(PMF_component (FST s) p
(FST (SND s)) = (SND (SND s)))

where p is the probability space and s is a tuple $(X_{i},j,p_{ij})$ stating
that a random state variable $X_{i}$ is in State $j$ and have probability
$p_{ij}$.

The following definition specifies all the pipeline segments.

######  Definition 6.2.

_Pipeline Segments_
$\vdash_{def}$ $\forall$p S SL.
component_state_pred p S SL =
(CDF_seg_list p
(seg_tuple_list S SL)) $\wedge$
(component_events_space S
(LENGTH SL) = p_space p)

where S represents the random state variable of segment and SL specifies the
list of state probability pairs of the form ${(j,p_{ij})}$ of the random state
variable S. The first predicate in above definition allocates the state
probabilities to the corresponding state events using the function
PMF_component while the second condition ensures that the list SL forms a
complete event space. The function seg_tuple_list takes the random variable S
and list of its state probability pairs of the form ${(j,p_{ij})}$ and returns
the list of tuples of the form ${(S,j,p_{ij})}$. The function CDF_seg_list
returns a list of component performances at all operational states obtained
from the function seg_tuple_list (Definition 6.4). These functions are
formally defined in HOL4 as follows:

######  Definition 6.3.

_List of Segment State Probabilities_
$\vdash_{def}$ ($\forall$p. CDF_seg_list p [] = T) $\wedge$
($\forall$p h t. CDF_seg_list p (h::t) =
CDF_seg p h $\wedge$ CDF_seg_list p t)

######  Definition 6.4.

_List of Segment Tuples_
$\vdash_{def}$ $\forall$p. seg_tuple_list X L =
MAP ($\lambda$a. (X,a)) L

Now, we formally model the complete pipeline, shown in Figure 3, operating as
the multistate series coherent system in HOL4 as:

######  Definition 6.5.

_Performance Distribution of Series Pipeline_
$\vdash_{def}$ $\forall$L p j.
PDF_pipeline_series L p j =
prob p (CDF_PHI_state_event
series_MS L p j)

The above formal specifications of the oil and gas pipeline allow us to reason
about the pipeline performance given the performance of its segments.

###  6.2 Formal Verification

Consider a pipeline having $10$ segments, depicted in Figure 3, where each
segment has states ranging from $0$ to $4$, i.e., there are $5$ operational
states for every segment of the pipeline. Let $p_{ij}$ be the performance of
the segment $i$ operating in State $j$. Similarly, the notation $P_{ij}$ be
the performance distribution of segment $i$ operating in any state
$j=0,1,\cdots,4$. Assuming all the segments are performing mutually
independent, then the performance distribution of the series pipeline can be
mathematically written as:

$P_{pipeline}(j)=P[pipeline\leq j]=1-\prod_{i=1}^{10}(1-P_{ij})$ (7)

$\begin{split}P_{pipeline}(j)&=1-\prod\limits_{i=1}^{10}\left(1-\sum\limits_{k=0}^{j}p_{i,k}\right)\\\
&=1-((1-(p_{1,0}+p_{1,1}+\cdots+p_{1,j}))*\\\ &\ \ \
(1-(p_{2,0}+p_{2,1}+\cdots+p_{2,j}))*\cdots*\\\ &\ \ \
(1-(p_{10,0}+p_{10,1}+\cdots+p_{10,j})))\end{split}$ (8)

Similarly, the performance distribution of the series pipeline operating in
the second state, i.e., State $1$ is mathematically expressed as follows:

$\begin{split}P_{pipeline}(1)&=1-\prod\limits_{i=1}^{10}\left(1-\sum\limits_{k=0}^{1}p_{i,k}\right)\\\
&=1-\prod\limits_{i=1}^{10}\left(1-p_{i,0}-p_{i,1}\right)\\\
&=1-((1-p_{1,0}-p_{1,1})*(1-p_{2,0}-p_{2,1})*\\\
&(1-p_{3,0}-p_{3,1})*(1-p_{4,0}-p_{4,1})*\\\
&(1-p_{5,0}-p_{5,1})*(1-p_{6,0}-p_{6,1})*\\\
&(1-p_{7,0}-p_{7,1})*(1-p_{8,0}-p_{8,1})*\\\
&(1-p_{9,0}-p_{9,1})*(1-p_{10,0}-p_{10,1}))\end{split}$ (9)

When the multistate system is in the first state, i.e., State $0$, it is in
complete failure mode. Therefore, the performance of segment $i$ operating in
State $0$ is equal to zero, i.e., $p_{i,0}=0$ for all $1\leq i\leq 10$. Using
$p_{i,0}=0$ in Equation (9) results in the following equation:

$\begin{split}P_{pipeline}(1)&=1-\prod\limits_{i=1}^{10}\left(1-\sum\limits_{k=0}^{1}p_{i,k}\right)\\\
&=1-\prod\limits_{i=1}^{10}\left(1-p_{i,0}-p_{i,1}\right)\\\
&=1-((1-p_{1,1})*(1-p_{2,1})*(1-p_{3,1})*\\\
&(1-p_{4,1})*(1-p_{5,1})*(1-p_{6,1})*\\\ &(1-p_{7,1})*(1-p_{8,1})*\\\
&(1-p_{9,1})*(1-p_{10,1}))\end{split}$ (10)

We formally verify the performance distribution for a series pipeline
(Equation (8)) in HOL4 as follows:

######  Theorem 6.1.

_Performance Distribution of Series Pipeline_
$\vdash_{thm}$ $\forall$SL pSL j p.
Let
val SL = [S1;S2;...;S10];
val pSL = [[p1_0;p1_1;...;p1_4];
[p2_0;p2_1;...;p2_4];...;
[p10_0;p10_1;...;p10_4]];
in
[A1:] prob_space p $\wedge$
[A2:] $\forall$l. MEM l (ZIP(SL,pSL))
$\Rightarrow$ component_state_pred
(FST l) p (SND l) $\wedge$
[A3:] ($\forall$l. MEM l SL
$\Rightarrow$ (CDF_rand_stat_event l
p j $\in$ events p)) $\wedge$
[A4:] mutual_indep p (MAP ($\lambda$a.
CDF_rand_stat_event a p j) SL)
$\Rightarrow$ (PDF_pipeline_series SL p j =
1 - ((1 - sum_list j
[p1_0;p1_1;...;p1_4])*
(1 - sum_list j
[p2_0;p2_1;...;p2_4])*$\cdots$*
(1 - sum_list j
[p10_0;p10_1;...;p10_4]))

where the list SL specifies the random state variables of all the segments.
The list pSL is the list of lists representing the performance of all the
pipeline segments operational states. Assumption A1 is the same as Assumption
A1 of Theorem 5.2. The function component_state_pred in Assumption A2 gives
the specifications of all the segments, i.e., all the random variables in the
list SL are assigned to their corresponding performances from the list pSL.
Assumptions A3 and A4 ensure that all the pipeline segments random state
variables have their events in the valid probability space p and are
statistically mutually independent. Finally, the conclusion of Theorem 6.1
models Equation (8). The function sum_list takes a number j and a list of
pairs and returns the sum of the second elements of first j pairs.

######  Definition 6.6.

_Sum of First $n$ Elements of List_
$\vdash_{def}$ ($\forall$n. sum_list n [] = []) $\wedge$
($\forall$n x xs. sum_list n (x::xs) =
if n = 0 then 0 else
(SND x) + sum_list (n - 1) xs)

The proof of Theorem 6.1 is carried out mainly using Theorems 5.1, 5.2 and 5.6
and is quite straightforward. It just took about $80$ lines of HOL4 code and a
few man-hours, which clearly illustrates the effectiveness of our proposed
framework. Finally, we formally verify the performance distribution of the
series pipeline operating in State $1$ (Equation (10)) as follows:

######  Theorem 6.2.

_Performance Distribution of Series Pipeline Operating in Second state, i.e.,
State $1$_
$\vdash_{thm}$ $\forall$SL pSL p.
Let
val SL = [S1;S2;...;S10];
val pSL = [[0;p1_1;...;p1_4];
[0;p2_1;...;p2_4];...;
[0;p10_1;...;p10_4]];
in
[A1:] prob_space p $\wedge$
[A2:] $\forall$l. MEM l (ZIP(SL,pSL))
$\Rightarrow$ component_state_pred
(FST l) p (SND l) $\wedge$
[A3:] ($\forall$l. MEM l SL
$\Rightarrow$ (CDF_rand_stat_event l
p 1 $\in$ events p)) $\wedge$
[A4:] mutual_indep p (MAP ($\lambda$a.
CDF_rand_stat_event a p 1) SL)
$\Rightarrow$ (PDF_pipeline_series SL p 1 =
1 - ((1 - p1_1) * (1 - p2_1) *
(1 - p3_1) * (1 - p4_1) *
(1 - p5_1) * (1 - p6_1) *
(1 - p7_1) * (1 - p8_1) *
(1 - p9_1) * (1 - p10_1))

The verification of the above theorem is mainly based on Theorem 6.2 and is
done almost automatically, which clearly illustrate the practical
effectiveness of our formally verified Theorem 6.1 having generic number of
segments and operating states of the multistate system. Thus, the verification
mainly involves specializing these generic variables to specific numbers of
operating states, such as, $2$ states in Theorem 6.2. More details about our
formal analysis of the multistate coherent systems can be found at our project
webpage projectwebperfanaly2021 .

Figure 4: Performance Distribution of Segment $i$ Operating in State $1$ with
$p_{i,1}=0.7$ (Above Average) for $i\geq 3$

We encoded our formalized Theorem 6.2 in Python, as given in Algorithm 1, for
different values of $p_{i,1}$, capturing the performance of segment $i$
operating in the second operational state, i.e., State $1$. It provides a
graphical representation of the performance distribution of the multistate
coherent oil and gas pipeline as shown in Figures 4 and 5. We set the values
of $p_{i,1}=0.7$ (above average) for $i\geq 3$, whereas, $p_{1,1}\in(0,1)$ and
$p_{2,1}\in(0,1)$ are represented on $x$ and $y$ axes in Figure 4. Whereas,
the $z$-axis depicts the performance distribution of Segment $i$ operating in
State $1$ that has its peak value (green color dot in Figure 4) at
$p_{1,1}=0.9226$ and $p_{2,1}=0.1015$. Similarly, Figure 5 captures the
performance distribution for a scenario, where $p_{i,1}=0.3$ (below average)
for $i\geq 3$, and $p_{1,1}\in(0,1)$ and $p_{2,1}\in(0,1)$. Moreover, the peak
of the performance distribution for this scenario exists at $p_{1,1}=0.00136$
and $p_{2,1}=0.1698$ and is represented by a green color dot in Figure 5.

1Input: performance_segment, N

2Output: Performance indicators: $p_{1,1}$ , $p_{2,1}$ , $P_{pipeline}(1)$

3//Initialization

4 product_performance = 1

5// Outer Loop for No. of trials

6for  _each, $j\in N$_ do

7

8 // Inner Loop to compute the product of performance, i.e.,

9 $\prod_{i=1}^{10}\left(1-p_{i,0}-p_{i,1}\right)$

10 for  _each, $i\in N$_ do

11 if  _ $\text{performance\\_segment}\left[i\right]<=1$_ then

12

13 product_performance = product_performance $\times$

14 (1 - performance_segment $\left[i\right]$)

15 end if

16

17 end for

18

19 // Computing performance distribution,

20 $P_{pipleline}(1)=1-\prod_{i=1}^{10}\left(1-p_{i,0}-p_{i,1}\right)$

21 $P_{pipeline}(j)=(1-\text{product\\_performance})$

22 $p_{1,1}=\text{choose\ probability\ between\ (0 , 1)}$

23 $p_{2,1}=\text{choose\ probability\ between\ (0 , 1)}$

24 product_performance = 1

25 end for

26

27return $([p_{1,1},p_{2,1},P_{pipeline}(1)])$

Algorithm 1 Performance Distribution of Segment i operating in State $1$
Figure 5: Performance Distribution of Segment $i$ Operating in State $1$ with
$p_{i,1}=0.3$ (Below Average) for $i\geq 3$

The distinguishing features of our proposed HOL formalization for the
performance analysis of the multistate coherent systems as compared to the
traditional analysis techniques are that it allows us to formally verify
generic expressions for multistate oil and gas pipelines, i.e., all of the
variables and functions are of generic nature, i.e., universally quantified,
presenting any number of segments, any number of operational states and
arbitrary probability distributions. Moreover, they can be specialized to
perform the formal performance analysis of any real-world multistate coherent
system. For example, Theorem 6.1 provides the analysis of a multistate oil and
gas pipeline system with $10$ number of segments and $5$ operational states.
Similarly, Theorem 6.2 presents the analysis of the same system operating in
State $1$. Whereas, in the case of simulation based analysis, we need to model
and analyze each system individually. Soundness is assured in functions and
theorems as every new theorem is verified by applying basic axioms and
inference rules or any other previously verified theorems/inference rules.
Moreover, this approach guarantees correctness of the analysis by ensuring
that all the necessary assumptions for the validity of the result are
explicitly present with the theorem. The above mentioned benefits are not
assured by any traditional approaches for performing the reliability analysis
of the multistate oil and gas pipelines systems that suffer from their
inherent limitations, such as, limited computational resources and human
error-proneness. Therefore, the reliability analysis presented in this paper
undoubtedly depicts the usefulness of the proposed methodology.

##  7 Conclusions

In this paper, we proposed a HOL theorem proving based framework for formally
analyzing the reliability of the multistate coherent systems. In particular,
we presented the HOL formalization of series and parallel multistate coherent
systems. Based on this formalization, we formally verified various
deterministic properties of these systems, such as, upper and lower bounds on
structure functions, relationship of redundancy at the component and system
levels and the compositional nature of the structure function. Next, we
formally verified the probabilistic properties, such as, system level
performance. This framework allowed us to formally verify generic mathematical
properties about multistate coherent systems with an arbitrary number of
components and their states. Finally, to demonstrate the practical
effectiveness of our proposed approach, we performed the formal reliability
analysis of the multistate oil and gas pipeline using the HOL4 theorem prover.

## References

  * (1) El-Neweihi E, Proschan F and Sethuraman J.  Multistate Coherent Systems.  _Journal of Applied Probability_ 1978; 15(4): 675–688.
  * (2) Ebrahimi N.  Multistate Reliability Models.  _Naval Research Logistics Quarterly_ 1984; 31(4): 671–680.
  * (3) Coroporation R.  Reliability Growth & Repairable System Analysis.  _Tucson: ReliaSoft Publishing_ 2009; .
  * (4) Menčík J.  Software for Reliability Analysis.  In _Concise Reliability for Engineers_. IntechOpen, 2016.
  * (5) Billinton R and Wenyuan L.  Hybrid Approach for Reliability Evaluation of Composite Generation and Transmission Systems using Monte-Carlo Simulation and Enumeration Technique.  _IEE Proceedings C - Generation, Transmission and Distribution_ 1991; 138(3): 233–241.  10.1049/ip-c.1991.0029.
  * (6) Zio E, Marella M and Podofillini L.  A Monte Carlo Simulation Approach to the Availability Assessment of Multi-state Systems with Operational Dependencies.  _Reliability Engineering & System Safety_ 2007; 92(7): 871–882.
  * (7) Hasan O and Tahar S.  Formal Verification Methods.  In _Encyclopedia of Information Science and Technology, Third Edition_. IGI Global, 2015.  pp. 7162–7170.
  * (8) Ahmad W.  _Formal Dependability Analysis using Higher-order-logic Theorem Proving_.  PhD Thesis, National University of Sciences & Technology (NUST) Islamabad, Pakistan, 2017.
  * (9) Trivedi KS.  _Probability and Statistics with Reliability, Queuing, and Computer Science Applications_ , volume 13.  Wiley Online Library, 1982.
  * (10) Ahmad W, Hasan O, Tahar S et al.  Formal Reliability Analysis of Oil and Gas Pipelines.  _Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability_ 2018; 232(3): 320–334.
  * (11) Ahmad W, Murtza SA, Hasan O et al.  On the Formalization of Importance Measures using HOL Theorem Proving.  In _Formal Methods in Software Engineering_. IEEE, pp. 109–118.
  * (12) Ahmad W and Hasan O.  Towards Formal Fault Tree Analysis using Theorem Proving.  In _Intelligent Computer Mathematics_. Springer, pp. 39–54.
  * (13) Ahmad W and Hasan O.  Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach.  In _Dependable Software Engineering: Theories, Tools, and Applications_. Springer, pp. 264–279.
  * (14) Zio E, Podofillini L and Levitin G.  Estimation of the Importance Measures of Multi-state Elements by Monte Carlo Simulation.  _Reliability Engineering & System Safety_ 2004; 86(3): 191–204.
  * (15) Ramirez-Marquez JE and Coit DW.  A Monte-Carlo Simulation Approach for Approximating Multi-state Two-terminal Reliability.  _Reliability Engineering & System Safety_ 2005; 87(2): 253–264.
  * (16) Caldarola L.  Coherent Systems with Multistate Components.  _Nuclear Engineering and Design_ 1980; 58(1): 127–139.
  * (17) Boedigheimer RA and Kapur KC.  Customer-driven Reliability Models for Multistate Coherent Systems.  _Transactions on Reliability_ 1994; 43(1): 46–50.
  * (18) Natvig B and Streller A.  The Steady-state Behaviour of Multistate Monotone Systems.  _Journal of Applied Probability_ 1984; 21(4): 826–835.
  * (19) Aven T and Jensen U.  _Stochastic Models in Reliability_.  Springer, 1999.
  * (20) Xue J and Yang K.  Dynamic Reliability Analysis of Coherent Multistate Systems.  _Transactions on Reliability_ 1995; 44(4): 683–688.
  * (21) Gordon M.  Mechanizing Programming Logics in Higher-order Logic.  In _Current Trends in Hardware Verification and Automated Theorem Proving_. Springer, pp. 387–439.
  * (22) Harrison J.  Formalized Mathematics.  Technical Report 36, Turku Centre for Computer Science, Finland, 1996.
  * (23) Gordon MJ and Melham TF.  _Introduction to HOL a theorem proving environment for higher-order logic_.  Cambridge University Press, 1993.
  * (24) Church A.  A Formulation of the Simple Theory of Types.  _Journal of Symbolic Logic_ 1940; 5: 56–68.
  * (25) Milner R.  A Theory of Type Polymorphism in Programming.  _Journal of Computer and System Sciences_ 1977; 17: 348–375.
  * (26) Paulson LC.  _ML for the Working Programmer_.  Cambridge University Press, 1996.
  * (27) Mhamdi T, Hasan O and Tahar S.  On the Formalization of the Lebesgue Integration Theory in HOL.  In _Interactive Theorem Proving_ , _LNCS_ , volume 6172\. Springer, 2011.  pp. 387–402.
  * (28) Zhang Z and Shao B.  Reliability Evaluation of Different Pipe Section in Different Period.  In _Service Operations and Logistics, and Informatics_ , volume 2. IEEE, pp. 1779–1782.
  * (29) Murtza SA.  Towards the Formal Performance Analysis of Multistate Coherent Systems using HOL Theorem Proving, 2021.  http://save.seecs.nust.edu.pk/projects/famcs/.