Modelling Smart Buildings Using Fault Maintenance Trees

Increasingly many industrial spheres are enforced by law to satisfy strict RAMS requirements-reliability, availability, maintain-ability, and safety. Applied to Fault Maintenance Trees (FMTs), formal methods offer flexible and trustworthy techniques to quantify the resilience of (abstract models of) systems. However, the estimated metrics are relevant only as far as the model reflects the actual system: Refining an abstract model to reduce the gap with reality is crucial for the usefulness of the results. In this work, we take a practical approach at the challenge by studying a Heating, Ventilation and Air-Conditioning unit (HVAC), ubiquitous in smart buildings. Using probabilistic and statistical model checking, we assess RAMS metrics of a basic fault maintenance tree HVAC model. We then implement four modifications augmenting the expressivity of the FMT model, and show that reliability, availability, expected number of failures, and costs, can vary by orders of magnitude depending on involved modelling details.