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

Alessandro Abate, Carlos Esteban Budde, Nathalie Cauchi, Khaza Anuarul Hoque, Mariëlle Ida Antoinette Stoelinga

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    34 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationProceedings of the European Conference of the PHM Society
    PublisherPHM society
    Number of pages16
    Volume4
    Edition1
    Publication statusPublished - 2 Jul 2018
    Event4th European Conference of the Prognostics and Health Management Society, PHME 2018 - Muntgebouw Utrecht, Utrecht, Netherlands
    Duration: 3 Jul 20186 Jul 2018
    Conference number: 4
    http://www.phmsociety.org/events/conference/phm/europe/18

    Publication series

    NameProceedings of the European Conference of the PHM Society
    PublisherPHM society

    Conference

    Conference4th European Conference of the Prognostics and Health Management Society, PHME 2018
    Abbreviated titlePHME 2018
    CountryNetherlands
    CityUtrecht
    Period3/07/186/07/18
    Internet address

      Fingerprint

    Keywords

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

    Cite this

    Abate, A., Budde, C. E., Cauchi, N., Hoque, K. A., & Stoelinga, M. I. A. (2018). Assessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees. In Proceedings of the European Conference of the PHM Society (1 ed., Vol. 4). (Proceedings of the European Conference of the PHM Society). PHM society.