-A A +A

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

TitleAssessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees
Publication TypeConference Paper
Year of Publication2018
AuthorsAbate A, Budde CE, Cauchi N, Hoque KAnuarul, Stoelinga M
Conference NameFourth european conference of the prognostics and health management society 2018
Date Published07/2018
Conference LocationUtrecht, Netherlands
KeywordsAvailability, fault maintenance trees, HVAC, Maintenance, Model Checking, probabilistic model checking, reliability, Smart Buildings, Statistical Model Checking

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.



Oxford Control and Verification (OXCAV) Group

C/O Department of Computer Science

Wolfson Building, Parks Rd, Oxford OX1 3QD

T: +44 (0) 18656 10767

Education - This is a contributing Drupal Theme
Design by WeebPal.