arXiv:1801.04263v1 [cs.LO] 12 Jan 2018

Efficient Probabilistic Model Checking
of Smart Building Maintenance using
Fault Maintenance Trees
Nathalie Cauchi1 , Khaza Anuarul Hoque1 , Alessandro Abate1 , and Mariëlle
Stoelinga2
1

2

Department of Computer Science, University of Oxford, Oxford UK
1
{name.surname}@cs.ox.ac.uk
Formal Methods and Tools Group, University of Twente, Twente, The
Netherlands
2
marielle@cs.utwente.nl

Abstract
Cyber-physical systems, like Smart Buildings and power plants, have
to meet high standards, both in terms of reliability and availability. Such
metrics are typically evaluated using Fault trees (FTs) and do not consider maintenance strategies which can significantly improve lifespan and
reliability. Fault Maintenance trees (FMTs) – an extension of FTs that
also incorporate maintenance and degradation models, are a novel technique that serve as a good planning platform for balancing total costs and
dependability of a system. In this work, we apply the FMT formalism to a
Smart Building application. We propose a framework for modelling FMTs
using probabilistic model checking and present an algorithm for performing abstraction of the FMT in order to reduce the size of its equivalent
Continuous Time Markov Chain. This allows us to apply the probabilistic
model checking more efficiently. We demonstrate the applicability of our
proposed approach by evaluating various dependability metrics and maintenance strategies of a Heating, Ventilation and Air-Conditioning system’s
FMT.

1

Introduction

Worldwide, buildings account for approximately 40% of the total energy consumption and 20% of the total CO2 emissions, annually [6]. Efficient Building Automation Systems (BAS) can reduce energy consumption by up to 30%
through their optimal operation, continuous commissioning and maintenance [6].
Constructions employing such technologies are termed Smart Buildings. High
standards have to be adhered by such technologies, both in terms of reliability
1

and availability. One way of achieving this is by employing methods to perform
preventative and predictive maintenance actions. Diagnostic and fault detection techniques for Smart Building applications have been developed in [15, 3].
Predictive and preventative maintenance strategies are devised in [5, 2]. However, these techniques preclude availability and reliability measurements and
focus only on synthesis of maintenance policies in the presence of degradation
and fault finding. Reliability and availability are typically tackled using Fault
Trees (FTs), where the focus is on finding the root causes of a system failure
using a top-down approach. FTs do not include maintenance strategies in the
analysis – a key element in reducing component failures. [14] presents the Fault
Maintenance Tree (FMT) as an extension of FT encompassing both degradation
and maintenance models. The degradation models represent the different levels
of component degradation and are known as Extended Basic Events (EBE).
The maintenance models incorporate the undertaken maintenance policy which
includes both inspections and repairs. These are modelled using Repair and
Inspection modules in the FMT framework.
In literature, FMTs are analysed using Statistical Model Checking technique
(SMC) [14] and provide statistical guarantees. In contrast, Probabilistic Model
Checking (PMC), based on numerical analysis, provide formal guarantees with
higher accuracy when compared with SMC [17]. However, numerical methods
are far more memory intensive and may result in a state space explosion. This
limitation of PMC often leaves SMC as the last resort [17]. In this paper we
tackle the FMT analysis using PMC. Our contributions can be summarised as
follows:
1. We formalise the FMT framework using Continuous Time Markov Chain
(CTMCs).
2. We formalise the dependability metrics using the extended Continuous
Stochastic Logic (CSL) formalism such that they can be computed using
the PRISM model checker [12].
3. To mitigate the state space explosion problem, we present an FMT abstraction technique which decomposes a large FMT into an equivalent abstract FMT based on our proposed graph decomposition algorithm. Using
our framework, we are able to achieve a 67% reduction in the state space
size.
4. Finally, we construct a FMT that identifies failure of a Heating, Ventilation and Air-conditioning system (HVAC). We apply the developed
framework to the built FMT and evaluate relevant dependability metrics,
together with different maintenance strategies using the PRISM model
checker.
To the best of our knowledge, this is the first attempt to analyse FMTs using
Probabilistic Model Checking and also the first application to Smart Building
systems.

2

This article has the following structure: Section 2 introduces the fault maintenance trees and probabilistic model checking frameworks. This is followed by
the developed methodology for modelling FMT using CTMCs and performing
model checking in Section 3. The framework is applied to a heating, ventilation
and air-conditioning (HVAC) case study which is presented in Section 4.

2

Preliminaries

2.1

Fault maintenance trees framework

Fault trees are directed acyclic graphs (DAG) describing the combinations of
component failures that lead to system failures. The leaves in the fault trees are
called basic events and denote the system failures. The internal nodes of the
graph are called gates and describe the different ways that failures can interact
to cause other components to fail. The gates in a fault tree can be of several
types and these include the AND gate, OR gate, k/N-gate [14].
Fault maintenance trees (FMT) extend fault trees by including maintenance
(all the standard FT gates are also employed by the FMTs). This is achieved
by making use of:
1. Extended Basic Events - The basic events are modified to incorporate
degradation models of the component the leaf represents. The degradation
models represent different discrete levels of degradations the components
can be in and are a function of time.
2. Rate Dependency Events - A new gate introduced in [14], labelled as
RDEP that accelerates the degradation rates of dependent child nodes
and is depicted in Figure 1. When the component connected to the input
of the RDEP fails, the degradation rate of the dependent components is
accelerated with an acceleration factor γ.
input

RDEP

Children (n)

Figure 1: RDEP gate with 1 input and dependent components also known as
children.
3. Repair and Inspection modules - The repair module (RM) performs cleaning or replacements actions. These actions can be either carried out using
fixed time schedules or when enabled by the inspection module (IM). The
IM performs periodic inspections and when components fall below a certain degradation threshold a repair or partial replacement is initiated by
the IM to be performed by the RM.

3

2.2

Probabilistic model checking

Model checking is a well-established formal verification technique used to verify
the correctness of finite-state systems. Given a formal model of the system
to be verified in terms of labelled state transitions and the properties to be
verified in terms of temporal logic, the model checking algorithm exhaustively
and automatically explores all the possible states in a system to verify if the
property is satisfiable or not. Probabilistic model checking deals with systems
that exhibit stochastic behaviour and is based on the construction and analysis
of a probabilistic model of the system. We make use of CTMCs, having both
transition and state labels, to perform stochastic modelling. Properties are
expressed in the form of extended Continuous Stochastic Logic (CSL) [11].
Definition 1 (Continuous time Markov chain (CTMC)) The tuple C =
(S, s0 , TL, AP, L, R) defines a CTMC which is composed of a set of states S,
the initial state s0 , a finite set of transition labels TL, a finite set of atomic
propositions AP, a labelling function L : S → 2AP and the transition rate
matrix R : S × S → R≥0 . The rate R(s, s0 ) defines the delay before which a
transition between states s and s0 takes place. If R(s, s0 ) 6= 0 then the probability
0
that a transition between the states s and s0 is defined as 1 − e−R(s,s )t where t
is time. No transitions will trigger if R(s, s0 ) = 0.
The logic of CSL specifies state-based properties for CTMCs, built out of propositional logic, a steady-state operator that refers to the stationary probabilities,
and a probabilistic operator for reasoning about transient state probabilities.
The state formulas are interpreted over states of a CTMC, whereas the path
formulas are interpreted over paths in a CTMC. For detail about the syntax and
semantics of CSL (which also includes reward formulae), we refer the interested
readers to [11].
Examples of a CSL property with its natural language translation are: (i)
P≥0.95 [F complete] - “The probability of the system eventually completing its
execution successfully is at least 0.95”. (ii) R=? [F success] - “What is the
expected reward accumulated before the system successfully terminates?”

3

Formalizing FMTs using CTMCs

In this section, we first formalise the FMT framework by presenting the formal
syntax and semantics for modelling FMTs using CTMCs. Next, we list the set
of metrics used to analyse the FMT. Finally, we present the developed framework which allows us to analyse large FMTs using probabilistic model checking
(PMC).

3.1

FMT Syntax

To formalise the syntax of FMTs using CTMCs, we first define the set F,
characterizing each FMT element by type, inputs and rates. We introduce a

4

new element called DELAY which will be used to model the deterministic time
delays required by the extended basic events (EBE), repair module (RM) and
inspection module (IM). We restrict the set Fto contain the EBE, RDEP gate,
OR gate, DELAY, RM and IM modules since these will be the components used
in the case study presented in Section 4.
Definition 2 (Elements of fault maintenance tree) The set Fof FMT elements consists of the following tuples. Here, n, N ∈ N are natural numbers, thresh, in, trig ∈ {0, 1} take binary values, Tdeg , Tcln , Trplc , Trep , Toh ,
Tinsp ∈ R≥0 are deterministic delays, and γ ∈ R≥0 is a rate.
• (EBE, Tdeg , Tcln , Trplc , N ) represent the extended basic events with N discrete degradation levels, each of which degrade with a time delay equal to
Tdeg . It also takes as inputs the time taken to restore the EBE to the
previous degradation level Tcln when cleaning is performed and the time
taken to restore the EBE to its initial state Trplc following a replacement
action.
• (RDEP, n, γ, in, Tdeg ) represents the RDEP gate with n dependent children, acceleration rate γ, the input in which activates the gate and Tdeg
the degradation rate of the dependent children.
• (OR, n) represents the OR gate with n inputs.
• (RM, n, Trep , Toh , Tinsp , Tcln , Trplc , thresh, trig) represents the RM module
which acts on n EBEs (in our case, this corresponds to all the EBEs
in the FMT). The RM can either be triggered periodically to perform a
cleaning action, every Trep delay, or a replacement action, every Toh delay,
or by the IM when the delay Tinsp has elapsed and the thresh condition
is met. The time to perform a cleaning action is Tcln , while the time
taken to perform a replacement is Trplc . The trig signal ensures that when
the component is not in the degraded states, no unnecessary maintenance
actions are carried out.
• (IM, n, Tinsp , Tcln , Trplc , thresh) represents the IM module which acts on
n EBEs (in our case, this corresponds to all the EBEs in the FMT).
The IM initiates a repair depending on the current state of the EBE.
Inspections are performed in a periodic manner, every Tinsp . If during an
inspection, the current state of the EBE does not correspond to the new
or failed state (i.e. the degradation level of the inspected EBE is below a
certain threshold), the thresh signal is activated and is sent to the RM.
Once a repair action is performed the IM moves back to the initial state
with a delay equal to Tcln or Trplc depending on the maintenance action
performed.
• (DELAY, T, N ) represents the DELAY module which takes two inputs
representing the deterministic delay T ∈ {Tdeg , Tcln , Trplc , Trep , Toh , Tinsp }
to be approximated using an Erlang distribution with N number of states.
5

This DELAY module can be extended by inclusion of a reset transition
label, which when triggered restarts the approximation of the deterministic
delay before it has elapsed. The extended DELAY module is referred to as
(DELAY, T, N )ext .
The FMT is defined as a special type of directed acyclic graph G = (V, E)
where the vertices V represent the gates and the events which represent an
occurrence within the system, typically the failure of a subsystem down to an
individual component level, and the edges E which represent the connections
between vertices. Events can either represent the EBEs or intermediate events
which are caused by one or more other events. The event at the top of the FMT
is the top event (TE) and corresponds to the event being analysed - modelling
the failure of the (sub)system under consideration. The EBE are the leaves of
the DAG. For G to be a well-formed FMT, we take the following assumptions (i)
vertices are composed of the OR, RDEP gates, (ii) there is only one top event,
(iii) RDEP can only be triggered by EBEs and (iv) RM and IM are not part of
the DAG tree but are modelled separately 1 . This DAG formulation allows us
to propose a framework in Subsection 3.5 such that we can efficiently perform
probabilistic model checking.
Definition 3 (Fault maintenance tree) A fault maintenance tree is a directed acyclic graph G = (V, E) composed of vertices V and edges E.

3.2

Semantics of FMT elements

Next, we provide the CTMC semantics for each FMT element f ∈ F. These
elements are then instantiated based on the underlying FMT structure to form
the semantics of the whole FMT in CTMC form.
DELAY We define the semantics for the (DELAY, T, N ) element using Figure 2(a) and describe the corresponding CTMC using the set of states given
by D = {d0 , d1 , . . . , dN +1 }, the initial state d0 , the set of transitions labels
TL = {trigger, move}, the set of atomic propositions AP = {T } with L(d0 ) =
· · · = L(dN ) = ∅, and L(dN +1 ) = {T }. The rate matrix R becomes clear from
Figure 2(a) and

µ i=0∧j =1



 N ((i ≥ 1 ∨ i < N + 1) ∧ j = i + 1)
(1)
Rij = T

∨(i = N + 1 ∧ j = 1)



0 otherwise,
with i representing the current state, j is the next state and µ is a fixed large
value corresponding to introducing a negligible delay, which is used to trigger
all the DELAY modules at the same time (cf. Definition 1). In Figure 2(b) we
1 Note, for different FMT structure same RM and IM modules are used, thus RM and IM
modules are independent of FMT structure

6

define the semantics of (DELAY, T, N )ext . This results in the CTMC described
using the state space D = {d0 , d1 , . . . , dN +1 }, the initial state d0 , the set of
transition labels TL = {trigger, move, reset}, the set of atomic propositions
AP = {T }, the labelling function L(d0 ) = L(d1 ) = · · · = L(dN ) = ∅, and
L(dN +1 ) = {T } and the rate matrix R where


µ i=0∧j =1





1 (i ≥ 2 ∨ i < N + 1) ∧ j = 1
(2)
Rij = N
((i ≥ 1 ∨ i < N + 1) ∧ j = i + 1)
T



∨(i = N + 1 ∧ j = 1)



0 otherwise,
with i representing the current state and j is the next state. In both instances,
the deterministic delays is approximated using an Erlang distribution [9] and all
DELAY modules are synchronised to start together using the trigger transition
label. The extended DELAY module have the transition labels reset which
restarts the Erlang distribution approximation whenever the guard condition
is met at a rate of 1 × Rsync where Rsync is the rate coming from the use of
synchronisation with other modules causing the reset to occur ( as explained
in Subsection 3.3). This is required when a maintenance action is performed
which restores the EBE’s state back to the original state and thus restart the
degradation process, before the degradation time has elapsed.
Remark 1 The basic properties of an Erlang distribution: A random variable
Z ∈ R+ has an Erlang distribution with k ∈ N stages and a rate λ ∈ R+ , Z ∼
Erlang(k, λ), if Z = Y1 + Y2 + . . . Yk where each Yi is exponentially distributed
with rate λ. The cumulative density function of the Erlang distribution is characterised using,
f (t; k, λ) = 1 −

k−1
X

1
exp(−λt)(λt)n
n!
n=0

for t, λ ≥ 0

(3)

and for k = 1, the Erlang distribution simplifies to the exponential distribution.
In particular, the sequence Zk ∼ Erlang(k, λk) converges to the deterministic
value λ1 for large k. Thus, we can approximate a deterministic delay T with
a random variable Zk ∼ Erlang(k, Tk ) [4]. Note, there is a trade-off between
the accuracy and the resulting blow-up in size of the CTMC model for larger
values of k (a factor of k increase in the model size) [9, 8]. In this work,
the Erlang distribution will be used to model the fixed degradation rates, the
maintenance and inspection signals. This is a similar approach taken in [14]
where degradation phases are approximated by an (k,λ)-Erlang distribution.
Extended Basic Events (EBE) The EBE are the leaves of the FMT and
incorporate the component’s degradation model. EBE are a function of the
total number of degradation steps N considered. Figure 3 shows the semantics
7

start

move, NT
trigger,µ

d0

d1

move, NT
d2

move, NT move, NT
...

d3

dN +1

move, NT
(a) CTMC representing DELAY with N states used to approximate a delay equal to
T approximated using Erlang(N, N
). The transition labels TL = {trigger, move}
T
are shown on each of the transitions. The state labels are not shown and the initial
state of the CTMC is pointed to using an arrow labelled with start.
start

move , NT
trigger ,µ

d0

d1

move , NT

d2
reset,1
reset,1

d3

move , NT move , NT
...

dN +1

reset,1
reset,1

(b) CTMC representing the extended DELAY with N states used to approximate a
delay equal to T . Delay approximated using Erlang(N, N
). The transition labels
T
TL = {trigger, move, reset} are shown on each of the state transitions, while the
state labels are not shown.

Figure 2: CTMC for (a) DELAY and (b) DELAY with reset guard.
of the (EBE, Tdeg , Tcln , Trep , N = 3). The corresponding CTMC is described
by the tuple ({s0 , s1 , s2 , s3 }, s0 , TLEBE , APEBE , LEBE , REBE ) where s0 is the
initial state ,
TLEBE = {degradei∈{0,...,N } , perform clean, perform replace},
the atomic propositions APEBE = {new , thresh, failed }, the labelling function
L(s
 0 ) = {new}, L(s1 ) = L(s2 ) = {thresh}, L(s3 ) = {f ailed} and REBE =
0
1
1
1

1
0
1
0

0
1
0
1

0
0
1
0

. The deterministic time delays taken as inputs are modelled using

three different DELAY modules:
1. an extended DELAY module approximating Tdeg with the transition label move replaced with degradeN such that synchronisation between the
two CTMCs is performed (explained in Subsection 3.3). When Tdeg has
elapsed the transition labelled with degradeN is triggered and the EBE
moves to the next state at a rate equal to TN
× 12 . The reset transition
deg
2 This

is a direct consequence of synchronisation and corresponds to R × REBE . Refer to

8

start
degrade1 , λ

s0

degrade2 , λ

perform clean, 1

s1

perform clean, 1

degrade3 , λ

s2

perform clean, 1

s3

perform replace, 1
perform replace, 1
perform replace, 1

Figure 3: CTMC representing the EBE with N = 3 with the transition labels
TLEBE = {degradei∈{1,2,3} , perform clean, perform replace} on each of the
state transitions. The state labels are not shown and the initial state is pointed
to by the arrow labelled with start.
label and corresponding transitions are replicated in extended DELAY
module and replaced with perform clean and perform replace. When
the corresponding maintenance action is performed one of the transition
label is triggered and the state of the EBE moves to previous state (if
cleaning action is carried out) or to the initial state (if replace action is
performed).
2. a DELAY module approximating Tcln with the transition label move replaced with perform clean. When Tcln has elapsed the transition with
transition label perform clean is triggered and the EBE moves to the
previous state at a rate equal to TN
.
cln
3. a DELAY module approximating Trplc with the transition label move replaced with perform replace. When Trplc has elapsed the transition
having the transition label perform replace is triggered and the EBE
N
moves to the initial state at a rate equal to Trplc
.
The transition labels perform clean and perform replace cannot be triggered
at the same time and it is assumed that Tcln 6= Trplc . This is a realistic assumption as only one maintenance action is performed at the same time.
RDEP gate The RDEP gate has static semantics and is used in combination
with the semantics of its n dependent EBEs. When triggered (in = 1), the
associated EBE reaches the state labelled failed , the degradation rate of the n
dependent children is accelerated by a factor γ. We model the in signal using,
(
1 L(s) = failed ,
in =
(4)
0 otherwise,
Subsection 3.3

9

where L(s) is the label of the current state of the associated EBE. Similarly,
we map the RDEP gate function using,
(
γTdeg1 , . . . , γTdegn in = 1,
(5)
RA =
Tdeg1 , . . . , Tdegn
otherwise,
where Tdegi , i ∈ 1, . . . n corresponds to the degradation rate of the n dependent
children. 3
OR gate The OR gate indicates a failure when either of its input nodes have
failed and also does not have semantics itself but is used in combination with
the semantics of its n dependent input events (EBEs or intermediate events).
We use,
(
0 E1 = 1 ∧ · · · ∧ En = 1
F AIL =
(6)
1 otherwise
where Ei = 1, i ∈ 1 . . . n corresponds to when the n events, connected to the
OR gate, represent a failure in the system. In the case of EBEs, E1 = 1 occurs
when the EBE reaches the failed state .
Repair module (RM) Figure 4 (a) shows the semantics of (RM, n, Trep , Toh ,
Tinsp , Tcln , Trplc , Trplc , thresh, trig). The CTMC is described using the state
space {rm0 , rm1 }, the initial state rm0 , the transition labels TLRM = {inspect,
check clean, check replace, trigger clean, trigger replace}, the atomic
propositions AP = {maintenance}, the labelling function L(rm0 ) = {∅}, L(rm1 ) =
{maintenance} and with RIM = [ 11 10 ]. For the sake of clarity in Figure 4 (a), we
used the transition labels check maintenance and trigger maintenance. The
transition label check maintenance and corresponding transitions are replicated and the transition labels replaced by check clean or check replace
to allow for both type of maintenance checks. Similarly, the transition label trigger maintenance and corresponding transitions are duplicated and
the transition labels replaced by trigger clean or trigger replace to allow the initiation of both type of maintenance actions to be performed. Due
to synchronisation, only one of the transitions may trigger at any time instance (as explained in Subsection 3.3). The transition labels trigger clean or
trigger replace correspond to the transition label trigger within the DELAY
module approximating the deterministic delays Tcln and Trplc respectively. The
deterministic delays which trigger inspect, check clean or check replace correspond to when the time delays Tinsp , Trep and Toh respectively, have elapsed.
All these signals are generated using individual DELAY modules with the move
transition label for each module replaced using inspect, check clean or check
3 Note, this effectively results in changing the deterministic delay being modelled by the
DELAY module to a new value if in = 1.

10

replace respectively. The thresh signal is modelled using,
(
1 L(sj,1 ) = thresh ∨ · · · ∨ L(sj,n ) = thresh,
thresh =
0 otherwise,

(7)

where L(sj,i ), j ∈ 0 . . . N, i ∈ 1 . . . n correspond to the label of the current state
j of each of the n EBE. Similarly, we model the trig signal using
(
1 L(sj,1 ) 6= new ∨ · · · ∨ L(sj,n ) 6= new ,
(8)
trig =
0 otherwise.
Both signals act as guards which when triggered determine which transition to
perform (cf. Fig. 4 (a)).
Inspection module (IM) The semantics of the (IM, n, Tinsp , Tcln , Trplc ,
thresh) is depicted in Figure 4 (b). The CTMC is defined using the tuple
({im0 , im1 }, im0 , TLIM , APIM , LIM , RIM ). Here,
TLIM = {inspect, perform clean, perform replace}
,
APIM = {∅}, L(s0 ) = L(s1 ) = ∅ and RIM = [ 11 10 ]. The thresh signal
corresponds to same signal used by the RM, given using (7). In Figure 4 (b),
for clarity, we use the transition label perform maintenance. This transition
label and corresponding transitions are duplicated and the transition labels
are replaced by either perform clean or perform replace to allow for both
type of maintenance actions to be performed when one of them is triggered
using synchronisation. The same DELAY modules used in the RM and EBE to
represent the deterministic delays are used by the IM. The DELAY module used
to represent the deterministic delays Tcln and Trplc triggers the transition labels
perform clean or perform replace. This represents that the maintenance
action has completed.

3.3

Semantics of FMT

Next, we show how to obtain the semantics of a FMT from the semantics of
its elements using the FMT syntax introduced in Subsection 3.1. We define
the DAG G by defining the vertices V and the corresponding events E. The
leaves of the DAG are the events corresponding to the EBE. The events E are
connected to the vertices V , which trigger the corresponding auxiliary function
used to represent the semantics of the gates. The Events connected to the RM
and IM are initiated by triggering the auxiliary functions thresh and trig given
using (7) and (8) respectively. Based on the structure of G, we compute the
corresponding CTMC by applying parallel composition of the individual CTMCs
representing the elements of the FMT. The parallel composition formulae are
derived from [7] and defined as follows,

11

inspect,thresh =0,1
check maintenance, trig=1,1
start

inspect, thresh =1,1

rm0

rm1

trigger maintenance,1
check maintenance, trig =0,1
(a)
CTMC
representing
the
RM
with
TLRM
=
{inspect, check maintenance, perform maintenance} shown on the state transitions. The guard condition trig = 0/1 or thresh = 0/1 must be satisfied for the
corresponding transition to trigger when it is activated via synchronisation with the
transition label.

inspect, thresh =0,1

start

inspect, thresh =1,1

im0

im1

perform maintenance ,1
(b) CTMC representing the IM with TLIM = {inspect, perform maintenance} shown
on the state transitions. The guard condition trig = 0 and thresh = 1 must be satisfied
for the corresponding transition to trigger when it is activated via synchronisation with
the transition label.

Figure 4: CTMC for (a) RM and (b) IM.
Definition 4 (Interleaving Synchronization) The interleaving synchronous
product of C1 = (S1 , s01 , TL1 , AP1 , L1 , R1 ) and C2 = (S2 , s02 , TL2 , AP2 , L2 , R2 )
is C1 ||C2 = (S1 × S2 , (s01 , s02 ), TL1 ∪ TL2 , AP1 ∪ AP2 , L1 ∪ L2 , R) where R is
given by:
α1 ,λ1

s1 −−−→ s01
α1 ,λ1

α2 ,λ2

s2 −−−→ s02

, and

(s1 , s2 ) −−−→ (s01 , s2 )

α2 ,λ2

,

(s1 , s2 ) −−−→ (s1 , s02 )

and s1 , s01 ∈ S1 , α1 ∈ TL1 , R1 (s1 , s01 ) = λ1 , s2 , s02 ∈ S2 , α2 ∈ TL2 , R2 (s2 , s02 ) =
λ2 .
Definition 5 (Full Synchronization) The full synchronous product of C1 =
(S1 , s01 , TL1 , AP1 , L1 , R1 ) and C2 = (S2 , s02 , TL2 , AP2 , L2 , R2 ) is C1 ||C2 =
(S1 × S2 , (s01 , s02 ), TL1 ∪ TL2 , AP1 ∪ AP2 , L1 ∪ L2 , R) where R is given by:
α,λ1

α,λ2

s1 −−−→ s01 and s2 −−−→ s02
α,λ1 ×λ2

(s1 , s2 ) −−−−−→ (s01 , s02 )
12

and s1 , s01 ∈ S1 , α ∈ TL1 ∧ TL2 , R1 (s1 , s01 ) = λ1 , s2 , s02 ∈ S2 , α2 ∈ TL2 ,
R2 (s2 , s02 ) = λ2 .
For any pair of states, synchronisation is performed either using interleaving
or full synchronisation. For full synchronisation, as in Definitions 4, the rate of a
synchronous transition is defined as the product of the rates for each transition.
The intended rate is specified in one transition and the rate of other transition(s)
is specified as 1. For instance, the RM synchronises using full synchronisation
with the DELAY modules representing Tinsp , Trep and Trplc and therefore, to
perform synchronisation between the RM and the DELAY modules, the rates
of all the transitions of RM should have a value of 1 (cf. Fig. 4 (a)), while
the rate of the DELAY modules represent the actual rates (cf. Fig 2). The
same principle holds for the EBEs and the IM. We refer the reader to Table 1
to further elucidate the synchronisation between the FMT components and the
method employed during the parallel composition.
Component
DELAY representing
RM
RM
EBE
DELAY representing
DELAY representing
DELAY representing
DELAY representing
DELAY representing
EBE

Tdeg

Tcln
Trplc
Tinsp
Trep
Toh

Synchronised with component
DELAY modules representing Tcln , Trplc , Tinsp
DELAY module representing Trep
DELAY module representing Toh
DELAY representing Tdeg
RM, EBE
RM, EBE
RM, IM
RM, IM, EBE
RM, IM, EBE
RM,IM, all DELAY modules, other EBEs

Transition label
trigger
trigger clean
trigger replace
degradeN
check clean
check replace
inspect
perform clean
perform replace
-

Synchronisation method
Full synchronisation
Full synchronisation
Full synchronisation
Full synchronisation
Full synchronisation
Full synchronisation
Full synchronisation
Full synchronisation
Full synchronisation
Interleave synchronisation

Table 1: Performing synchronisation between the different FMT components
and the synchronisation method used.
Example 1 (Synchronisation of FMT elements) Consider, a simple example showing the time signals and synchronisations required for modelling an
EBE and the RM and IM. The EBE has a degradation rate equal to Tdeg and we
limit the functionality of the RM and IM by allowing only the maintenance action to perform cleaning. We also need the corresponding DELAY modules generating the degradation rates, Tdeg and the maintenance rates Tcln , Tinsp , Trep .
The resulting CTMC is obtained by performing a parallel composition of the
components Call = CEBE || CTdeg ||CRM ||CIM ||CTcln ||CTinsp ||CTrep . The resulting state space is then Sall = SEBE ×STdeg ×SRM ×SIM ×STcln ×STinsp ×STrep .
The synchronisation between the different components is shown in Figure 5 and
proceeds as follows:
1. All the DELAY modules (except Tcln ) start at the same time using the
trigger transition label.
2. When the extended DELAY module generating the Tdeg time delay elapses,
the corresponding EBE moves to the next state through synchronisation
with the transition label degradeN .

13

3. The clock signals Trep , Tinsp represent periodic maintenance and inspection actions and when the deterministic delay is reached, through synchronisation with the transition label check clean or the inspect, the
RM or IM modules is triggered (cf. Fig. 4(a) and 4(b)). If RM triggers
a maintenance action, the DELAY representing Tcln is triggered using
the synchronisation labels trigger clean. Once the deterministic delay
Tcln elapses, the EBE, the extended DELAY module representing Tdeg
(where the reset transition label within the extended DELAY module is
replaced with perform clean ) and the IM are reset using the transition
label perform clean.

Figure 5: Block diagram showing the synchronisation connections between one
component and the other, together with the corresponding transition label which
trigger synchronisation.

Remark 2 One should note that this results in the requirement of a large state
space, which is a function of the number of states used to approximate the deterministic delays. Thus, to counteract this effect we propose an abstraction
framework in Subsection 3.5.

3.4

Metrics

We use PRISM to compute the metrics of the model described in Subsection
2.1. The metrics can be expressed using the extended Continuous Stochastic
Logic (CSL) as follows:
1. Reliability : This can be expressed as the complement of the probability
of failure over the time T , 1 − P=? [F≤T f ailed].
2. Availability: This can be expressed as R=? [C ≤T ]/T , which corresponds to
the cumulative reward of the total time spent in states labelled with okay
and thresh during the time T .

14

3. Expected cost: This can be expressed using R=? [C ≤T ], which corresponds
to the cumulative reward of the total costs (operational, maintenance and
failure) within the time T .
4. Expected number of failure: This can be expressed using R=? [C ≤T ], which
corresponds to the cumulative transition reward that counts the number
of times the top event enters the failed state within the time T .

3.5

Decomposition of FMTs

The use of CTMC and deterministic time delays results in the requirement of
a large state space for modelling the whole FMT (cf. Remark 2). We therefore
propose an approach which decomposes the large FMT into an equivalent abstract CTMC which can be analysed using PRISM. The process involves two
transformation steps. First we convert the FMT into the equivalent directed
acyclic graph (DAG) and split this graph into a set of smaller sub-graphs. Second, we transform the sub-graphs into the equivalent CTMC by making use
of the developed FMT components semantics (cf. Subsec. 3.2), and performing
parallel composition of the individual FMT components based on the underlying
structure of the sub-graph. The smaller sub-graphs are then sequentially recomposed to generate the higher level abstract FMT. Figure 6 depicts a high-level
diagram of the decomposition procedure.
ORIGINAL
FMT

EQUIVALENT
GRAPH

GRAPH
DECOMPOSITION

PMC
OF SUB-GRAPHS

PMC OF FINAL
CTMC

G1

G1

G3

G2

G1
G1

G2
G2

G3

G2

G3

B1

B3

B2

G2

B4

B1

MTTF(G2)

B2

DEPENDABILITY,
COSTS TRADE-OFFs

RDEP

B1

B2

B3

B4

B2

RDEP

G3

B3

B4

MTTF(G3)

G3

FINAL CTMC

RDEP

B2

LIBRARY OF CTMC MODELS

PARALLEL
COMPOSITION

CSL
PROPERTIES

CSL
PROPERTIES

Figure 6: Overall developed framework for decomposition of FMTs into the
equivalent abstract CTMCs.

Conversion of original FMT to the equivalent graph The FMT is a
DAG (cf. Subsection 3) and in this framework we need to apply a transformation
to the DAG in the presence of an RDEP gate, such that we can perform the
decomposition. The RDEP causes an acceleration of events on dependent child
nodes when the input node fails. In order to capture this feature in a DAG, we
need to duplicate the input node such that it is connected directly to the RDEP
15

vertex. This allows us to capture when the failure of the input occurs and the
corresponding acceleration of the the children. This is reasonable as the same
RM and IM are used irrespective of the underlying FMT structure.
Graph decomposition We define modules within the DAG as sub-trees composed of at least two events which have no inputs from the rest of the tree and no
outputs to the rest except from its output event [13]. We can divide the graph
into multiple partitions based on the number of modules making up the DAG.
We define the following notations to ease in the description of the algorithm:
• Vo indicates whether the node is the top node of the DAG.
• Vg indicates the node where graph split is performed.
• Modules correspond to sub-graphs in DAG.
We set Vo when we construct the DAG from the FMT and then proceed with
executing Algorithm 1. We first identify all the sub-graphs within the whole
DAG and label all the top nodes of each sub-graph i as VT i . We loop through
each sub-graph and its immediate child (the sub-graph at immediate lower level)
and at the point where the sub-graph and child are connected, the two graphs
are split and a new node Vg is introduced. Thus, executing Algorithm 1 results
in a set of sub-graphs linked together by the labelled nodes Vg . For each of lower
level sub-graphs we now proceed to compute the mean time to failure (MTTF).
This will serve as an input to the higher-level sub-graphs such that metrics for
the abstract equivalent CTMC can be computed.
Algorithm 1: DAG decomposition algorithm
input : DAG G = (V, E)
output: Set of sub-graphs with one of the end nodes labelled as Vg .
1 Identify sub-graphs using ‘depth-first’ traversal
2 Label all top nodes of each sub-graph i as VTi
3 forall select the top node of every sub-graph and immediate child defined
at immediate lower level do
4
if label VT already found in one of the leaf nodes of sub-graph then
5
Split sub-graph
6
Insert new node Vg which will be used as input from connected
sub-graph

PMC of sub-graphs We start from the bottom level sub-graphs and perform
the conversion to CTMC using the formal models presented in Subsection 3.2.
The formal models have been built into a library of PRISM modules and based
on the underlying components and structure making up the sub-graph, the corresponding individual formal models are converted into the sub-graph’s equivalent CTMC by performing parallel composition (cf. Subsec. 3.3). For each
16

sub-graph, we compute the probability of failure De (T ) at time T , from which
e (T ))
we calculate the MTTF using, MTTF = ln(1−D
. The MTTF serves as the
−T
input to the higher level sub-graph at time T . The new node in the higher-level
sub-graph, now degrades with the a new time delay Tdeg = MTTF , which is fed
into the corresponding DELAY component. This process is repeated for all the
different sub-graphs until the top level node Vo is reached.
PMC of final equivalent abstract CTMC On reaching the top level node
Vo , we compute the metrics for the equivalent abstract CTMC for a specific time
horizon T . For different horizons, the previous step of computing the MTTF
for the underlying lower level sub-graphs needs to be repeated. Using this
technique, we can formally verify larger FMTs, while using less memory and
computational time due to significantly smaller state space of the underlying
CTMCs. Next, we proceed with an illustrative example comparing the process
of directly modelling the large FMT using CTMCs versus the de-compositional
modelling procedure. Figure 7 presents the FMT composed of two modules and
the corresponding abstracted FMT. The abstract FMT is a pictorial representation of the moel represented by the equivalent abstract CTMC obtained using
the developed decomposition framework (cf. Fig. 6). For both the large FMT

Figure 7: The original FMT and the abstract FMT corresponding to the equivalent abstract CTMC generated by the developed framework. The MTTF for
the F’ is computed based on the probability of failure of the heating coil.
and the equivalent abstract FMT a comparison between the total number of
states for the resulting CTMC models, the total time to compute the reliability
metric and the resulting reliability metric is performed. All computations are
run on an 2.3 GHz Intel Core i5 processor with 8GB of RAM and the resulting
statistics are listed in Table 2. The original FMT has a state space with 193543
states, while the equivalent abstract CTMC has a state space with 63937 states.
This corresponds to a 67% reduction in the state space size. The total time to
17

compute the reliability metric is a function of the final time horizon and a maximal 73% reduction in computation time is achieved. Accuracy in the reliability
metric of the abstract model is a function of the time horizon. The accuracy
of the reliability metric computed by the abstract FMT results in a maximal
reduction of 0.61%.
Time
Horizon
(years)
5
10
15

Original FMT
Time to compute Reliability
metric
(mins)
0.727
0.9842
1.406
0.8761
2.489
0.3290

Abstracted FMT
Time to compute
Total
Reliability
MTTF metric
Time
(mins)
(mins)
(mins)
0.142
0.181
0.223
0.9842
0.219
0.309
0.528
0.8769
0.292
0.622
0.914
0.3270

Table 2: Comparison between the original large FMT and the abstracted FMT.

4

Case study

We apply the FMT framework to a Heating, Ventilation and Air-conditioning
(HVAC) system used to regulate a building’s internal environment. The HVAC
system under consideration for the FMT analysis is presented in Figure 8. It
is composed of two circuits - the air flow circuitry and the water circuit. The
gas boiler heats up the supply water which is fed into the heat pump. The heat
pump transfers the supply water into two sections - the supply air heating and
cooling coils and the radiators - via the splitter. The rate of water flowing in the
heating coil is controlled using a heating coil valve, while the rate of water flow
in the radiator is controlled using a separate valve. The outside air is mixed
with the extracted room air temperature via the mixer. This is fed into the
heating coil, which warms up the input air to the desired supply air temperature.
This air is supplied back, at a rate controlled by the Air Handling unit (AHU)
dampers, into the zone via the supply fan. The radiators are directly connected
to the water circuitry and transfer the heat from the water into the zone. The
return water is then passed through the collector and is returned back to the
boiler. Based on this HVAC system we construct the corresponding FMT shown
Mixer
Outside Air Intake
Heating
coil valve

Boiler

Heat
Pump

Heating &
cooling coil

Dampers

Supply Fan

Zone

Splitter
Radiator

Collector

Radiator valve
Air Input

Water Input

Figure 8: High level schematic of an HVAC system.
in Figure 9. The leaves of the tree are EBE with discrete degradation rates
18

computed using Table 3, approximated by the Erlang distribution where N is the
number of degradation phases (k = N for the Erlang distribution) and MTTF
is the expected time to failure with M T T F = 1/λ (cf. Remark 1). We choose
an acceleration factor γ = 2 for the RDEP gate. The system is periodically
repaired every 6 months (Trep = 182 days) and a major overhaul with a complete
replacement of all components is carried out once every 20 years (Toh = 20 ×
365 days). Weekly inspections are performed (Tinsp = 7 days) which return the
components back to the previous state. Only cleaning actions are performed
when inspections are carried out. The total time to perform a cleaning action is
1 day (Tcln = 1 day), while performing a total replacement of components takes
7 days (Trplc = 7 days). The time timing signals {Trep , Toh , Tinsp , Tcln , Trplc }
are all approximated using the Erlang distribution with N = 3. All maintenance
actions are performed simultaneously on all components.
Failure of HVAC component

Reduced
Capacity

No heating /
cooling

Failure in
Heating coil

8

9

Failure of
Supply Fan

1

RDEP

3

4

2

5

Insufficient
Radiator Pout

6

7

Figure 9: FMT for failure in HVAC system with leaves represented using EBE
(associated RM and IM not shown in figure). The EBE are labelled to correspond to the component failure they represent using the fault index presented
in Table 3.

4.1

Quantitative results

We make use of the developed framework (cf. Subsec. 3.5) and convert the
FMT representing the failure of the HVAC system (cf. Fig. 9) into the equivalent abstract CTMC. The abstracted CTMC has a state space of 62779 states.
Using our current computing set-up, the complex CTMC representing the whole
FMT was not computable as it results in a state space explosion. Highlighting, the advantage of the developed framework. The process is performed over

19

Fault Index

Failure Mode

N

1
2
3
4
5
6
7
8
9

Failure in cooling coil
Broken AHU Damper
Fan motor failure
Obstructed supply fan
Fan bearing failure
Radiator failure
Radiator stuck valve
Heater stuck valve
Failure in heat pump

4
2
3
4
6
4
2
2
4

MTTF
(years)
20
20
35
31
17
25
10
10
20

Table 3: Extended Basic events in FMT with associated degradation rates (N,
MTTF) obtained from [1, 10].

1
0.8
0.6
0.4
0.2
0

0

10

R{“Avail00 }=? [C ≤T ]/T

1-P=? [≤T f ailed]

six time horizons Nr = {0, 5, 10, 15, 20, 25} years with the maintenance policy
consisting of periodic cleaning every 6 months, a major overhaul every 20 years
and inspections on a weekly basis. For this set-up, the metrics corresponding to
the reliability and availability of the HVAC systems over the time horizon are
computed and are shown in Figure 10(b). The maximal time taken to compute
a metric using the abstract FMT is 1.47 minutes. It is deduced that both the
reliability and availability reduce over time and there is a saturation in the number of maintenance actions which one can perform before the system no longer
achieves higher performance in reliability and availability. Next, we compare

20

Time (Years)

1
0.8
0.6
0.4

0

10

20

Time (Years)

(a) Reliability of HVAC system.

(b) Availability of HVAC system.

Figure 10: Reliability and availability of HVAC over time horizon Nr .
the total cost of maintenance and the expected number of failures over the time
horizon Nr = {0, 5, 10, 15, 20, 25} years when considering different maintenance
strategies, such that we can identify the maintenance strategy that minimises
cost and the number of failures over time. We consider six different maintenance strategies which are listed in Table 4. The total maintenance cost to
perform a repair is 100 [GBP], while a replacement costs 5000 [GBP]. We now
compute the total expected maintenance costs and the total expected number
20

of failures for each strategy. These are shown in Figure 11. The most effective
strategy which offers a good trade-off between maintenance costs and the expected number of failures is achieved when repairs are carried out on a yearly
basis, replacements are carried out every 20 years and inspections are carried
out weekly (corresponding to strategy M1 ). Furthermore, it can be seen that the
frequency of inspections has a large effect on the total number of failures. When
the frequency of inspection is low (as in M4 and M5 ), the expected number of
component failures increases significantly. Note that reducing the periodicity of
repairs, as in the case of maintenance strategy M2 also results in an increase in
the expected number of failures.
Strategy index
M0
M1
M2
M3
M4
M5

Trep
6 months
12 months
48 months
6 months
6 months
6 months

20
20
20
10
20
20

Toh
years
years
years
years
years
years

Tinsp
1 Week
1 Week
1 Week
1 Week
2 years
5 years

Table 4: Implemented maintenance strategies

·10

1.5

M1

M2

1
0.5
0

0

M3
Expected number
of failures

R{“Costs00 }=? [C ≤T ]

M0
4

10

20

M4

M5

0.2
0.15
0.1
0.05
0

5

10

15

20

25

Time (years)

Time (years)

(b) Expected number of failures.

(a) Maintenance Costs.

Figure 11: Comparison between different number of maintenance strategies for
an HVAC systems.

5

Conclusion and Future Works

The paper has presented a methodology for applying probabilistic model checking to FMTs. The FMTs are modelled in the form of CTMCs which simplifies the transformation of FMT into formal models that can be analysed using
PRISM. A novel technique for abstracting the equivalent CTMC model is also
presented. The novel decomposition procedure tackles the issue of state space
explosion and results in a significant reduction in both the state space size and
21

the total time required to compute metrics. The framework has been applied to
an HVAC system and the effect of applying different maintenance strategies has
been presented. The presented framework can be further enhanced by adding
more gates to the PRISM modules library which include the Priority-AND, INHIBIT, k/N gates and to incorporate lumping of states as in [16], such that
the state space can be further reduced.

References
[1] Handbook ASHRAE. HVAC systems and equipment. American Society
of Heating, Refrigerating, and Air Conditioning Engineers, Atlanta, GA,
1996.
[2] Vladimir Babishin and Sharareh Taghipour. Optimal maintenance policy for multicomponent systems with periodic and opportunistic inspections and preventive replacements. Applied Mathematical Modelling,
40(24):10480–10505, 2016.
[3] Francesca Boem, Riccardo MG Ferrari, Christodoulos Keliris, Thomas
Parisini, and Marios M Polycarpou. A distributed networked approach for
fault detection of large-scale systems. IEEE Transactions on Automatic
Control, 62(1):18–33, 2017.
[4] Luca Bortolussi and Jane Hillston. Fluid approximation of CTMC with
deterministic delays. In Quantitative Evaluation of Systems (QEST), 2012
Ninth International Conference on, pages 53–62. IEEE, 2012.
[5] Nathalie Cauchi, Karel Macek, and Alessandro Abate. Model-based predictive maintenance in building automation systems with user discomfort.
Energy, 2017.
[6] European Parliament and Council of the European Union.
2010/31/EU, 2010.

Directive

[7] Holger Hermanns and Lijun Zhang. From concurrency models to numbers.
In Nato Science for Peace and Security Series. IOS Press, 2011.
[8] Khaza Anuarul Hoque, O Ait Mohamed, Yvon Savaria, and Claude
Thibeault. Probabilistic model checking based dal analysis to optimize
a combined tmr-blind-scrubbing mitigation technique for FPGA-based
aerospace applications. In Formal Methods and Models for Codesign
(MEMOCODE), 2014 Twelfth ACM/IEEE International Conference on,
pages 175–184. IEEE, 2014.
[9] Khaza Anuarul Hoque, Otmane Ait Mohamed, and Yvon Savaria. Towards
an accurate reliability, availability and maintainability analysis approach
for satellite systems based on probabilistic model checking. In Proceedings
of the 2015 Design, Automation & Test in Europe Conference & Exhibition,
pages 1635–1640. EDA Consortium, 2015.
22

[10] Faisal I Khan and Mahmoud M Haddara. Risk-based maintenance (rbm): a
quantitative approach for maintenance/inspection scheduling and planning.
Journal of Loss Prevention in the Process Industries, 16(6):561–573, 2003.
[11] Marta Kwiatkowska, Gethin Norman, and David Parker. Stochastic model
checking. In International School on Formal Methods for the Design of
Computer, Communication and Software Systems, pages 220–270. Springer,
2007.
[12] Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0:
Verification of probabilistic real-time systems. In G. Gopalakrishnan and
S. Qadeer, editors, Proc. 23rd International Conference on Computer Aided
Verification (CAV’11), volume 6806 of LNCS, pages 585–591. Springer,
2011.
[13] ZF Li, Yi Ren, LL Liu, and ZL Wang. Parallel algorithm for finding modules
of large-scale coherent fault trees. Microelectronics Reliability, 55(10):1400–
1403, 2015. Proceedings of the 26th European Symposium on Reliability of
Electron Devices, Failure Physics and AnalysisSI:Proceedings of {ESREF}
2015.
[14] Enno Ruijters, Dennis Guck, Peter Drolenga, and Mariëlle Stoelinga. Fault
maintenance trees: reliability centered maintenance via statistical model
checking. In Reliability and Maintainability Symposium (RAMS), 2016
Annual, pages 1–6. IEEE, 2016.
[15] Ying Yan, Peter B Luh, and Krishna R Pattipati. Fault diagnosis of
hvac air-handling systems considering fault propagation impacts among
components. IEEE Transactions on Automation Science and Engineering,
14(2):705–717, April 2017.
[16] Olexandr Yevkin. An efficient approximate markov chain method in dynamic fault tree analysis. Quality and Reliability Engineering International,
2015.
[17] Håkan LS Younes, Marta Kwiatkowska, Gethin Norman, and David Parker.
Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer, 8(3):216–228, 2006.

23

