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

19 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

Intelligent buildings
Formal methods
Availability
Costs
Fault tree analysis
Maintainability
Model checking
Air conditioning
Ventilation
Power plants
Inspection

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.
Abate, Alessandro ; Budde, Carlos Esteban ; Cauchi, Nathalie ; Hoque, Khaza Anuarul ; Stoelinga, Mariëlle Ida Antoinette. / Assessment of Maintenance Policies for Smart Buildings : Application of Formal Methods to Fault Maintenance Trees. Proceedings of the European Conference of the PHM Society. Vol. 4 1. ed. PHM society, 2018. (Proceedings of the European Conference of the PHM Society).
@inproceedings{b830945ad43045c3bdeb040f91f84732,
title = "Assessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees",
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 Markovchains 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.",
keywords = "Fault Maintenance Trees, Reliability, Availability, Maintenance, Model Checking, Probabilistic Model Checking, Statistical Model Checking, Smart Buildings, HVAC",
author = "Alessandro Abate and Budde, {Carlos Esteban} and Nathalie Cauchi and Hoque, {Khaza Anuarul} and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
year = "2018",
month = "7",
day = "2",
language = "English",
volume = "4",
series = "Proceedings of the European Conference of the PHM Society",
publisher = "PHM society",
booktitle = "Proceedings of the European Conference of the PHM Society",
edition = "1",

}

Abate, A, Budde, CE, Cauchi, N, Hoque, KA & Stoelinga, MIA 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 edn, vol. 4, Proceedings of the European Conference of the PHM Society, PHM society, 4th European Conference of the Prognostics and Health Management Society, PHME 2018, Utrecht, Netherlands, 3/07/18.

Assessment of Maintenance Policies for Smart Buildings : Application of Formal Methods to Fault Maintenance Trees. / Abate, Alessandro; Budde, Carlos Esteban; Cauchi, Nathalie; Hoque, Khaza Anuarul; Stoelinga, Mariëlle Ida Antoinette.

Proceedings of the European Conference of the PHM Society. Vol. 4 1. ed. PHM society, 2018. (Proceedings of the European Conference of the PHM Society).

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

TY - GEN

T1 - Assessment of Maintenance Policies for Smart Buildings

T2 - Application of Formal Methods to Fault Maintenance Trees

AU - Abate, Alessandro

AU - Budde, Carlos Esteban

AU - Cauchi, Nathalie

AU - Hoque, Khaza Anuarul

AU - Stoelinga, Mariëlle Ida Antoinette

PY - 2018/7/2

Y1 - 2018/7/2

N2 - 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 Markovchains 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.

AB - 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 Markovchains 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.

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

M3 - Conference contribution

VL - 4

T3 - Proceedings of the European Conference of the PHM Society

BT - Proceedings of the European Conference of the PHM Society

PB - PHM society

ER -

Abate A, Budde CE, Cauchi N, Hoque KA, Stoelinga MIA. 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. PHM society. 2018. (Proceedings of the European Conference of the PHM Society).