Efficient Probabilistic Model Checking of Smart Building Maintenance using Fault Maintenance Trees

TL;DR

This paper introduces a probabilistic model checking framework for Fault Maintenance Trees (FMTs) applied to smart building systems, enabling efficient evaluation of dependability metrics and maintenance strategies.

Contribution

It presents a novel probabilistic model checking approach for FMTs, including an abstraction algorithm to reduce model complexity for smart building applications.

Findings

Efficient evaluation of dependability metrics for HVAC systems.

Effective comparison of maintenance strategies using FMTs.

Demonstrated scalability of the approach with reduced model sizes.

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.