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.

Assessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees / Abate, Alessandro; Budde, Carlos E.; Cauchi, Nathalie; (Khaza Anuarul), Hoque; Stoelinga, Mariëlle. - ELETTRONICO. - 4:1(2018). (Intervento presentato al convegno European Conference of the PHM Society 2018 tenutosi a The Netherlands nel 2018).

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

Carlos E. Budde;
2018-01-01

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.
2018
Proceedings of the European Conference of the PHM Society 2018
The Netherlands
PHM society
Abate, Alessandro; Budde, Carlos E.; Cauchi, Nathalie; (Khaza Anuarul), Hoque; Stoelinga, Mariëlle
Assessment of Maintenance Policies for Smart Buildings: Application of Formal Methods to Fault Maintenance Trees / Abate, Alessandro; Budde, Carlos E.; Cauchi, Nathalie; (Khaza Anuarul), Hoque; Stoelinga, Mariëlle. - ELETTRONICO. - 4:1(2018). (Intervento presentato al convegno European Conference of the PHM Society 2018 tenutosi a The Netherlands nel 2018).
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314791
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact