Assessment of Maintenance Policies for Smart Buildings Application of Formal Methods to Fault Maintenance Trees



Published Jun 30, 2018
Alessandro Abate Carlos Esteban Budde Nathalie Cauchi Khaza Anuarul Hoque Mariëlle Stoelinga


Cyber-physical systems must meet high RAMS—reliability, availability, maintainability, and safety—standards. It is of essence to implement robust maintenance policies that decrease system downtime in a cost-effective way. Power plants and smart buildings are prominent examples where the cost of periodic inspections is high, and should be mitigated without compromising system reliability and availability. Fault Maintenance Trees (FMTs), a novel extension in fault tree analysis, can be used to assess system resilience: FMTs allow reasoning about failures in the presence of maintenance strategies, by encoding fault modes in a comprehensible and "maintenance-friendly" manner. A main concern is how to build a concrete model from the FMT, in order to compute the relevant RAMS metrics via (ideally automatic) analyses. Formal methods offer automated and trustworthy techniques to tackle with such task. In this work, we apply quantitative model checking—a well established formal verification technique—to analyse the FMT of a Heating, Ventilation and Air-Conditioning unit from a smart building. More specifically, we model the FMT in terms of continuous-time Markov
chains and priced time automata, which we respectively analyse using probabilistic and statistical model checking. In this way we are capable of automatically estimating the reliability, availability, expected number of failures, and differentiated costs of the FMT model for various time horizons and maintenance policies. We further contrast the two approaches we use, and identify their advantages and drawbacks.

How to Cite

Abate, A., Budde, C. E., Cauchi, N., Hoque, K. A., & Stoelinga, M. (2018). Assessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees. PHM Society European Conference, 4(1).
Abstract 1158 | PDF Downloads 421



Fault Maintenance Trees, Reliability, Availability, Maintenance, Model Checking, Probabilistic Model Checking, Statistical Model Checking, Smart Buildings, HVAC

Technical Papers