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.
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 language | English |
---|---|
Title of host publication | PHME 2018 |
Subtitle of host publication | Proceedings of the European Conference of the PHM Society 2018 |
Editors | Chetan S. Kulkarni, Tiedo Tinga |
Publisher | PHM Society |
Number of pages | 16 |
DOIs | |
Publication status | Published - 2 Jul 2018 |
Event | 4th European Conference of the Prognostics and Health Management Society, PHME 2018 - Muntgebouw Utrecht, Utrecht, Netherlands Duration: 3 Jul 2018 → 6 Jul 2018 Conference number: 4 http://www.phmsociety.org/events/conference/phm/europe/18 |
Publication series
Name | Proceedings of the European Conference of the PHM Society |
---|---|
Publisher | PHM Society |
Number | 1 |
Volume | 4 |
Conference
Conference | 4th European Conference of the Prognostics and Health Management Society, PHME 2018 |
---|---|
Abbreviated title | PHME 2018 |
Country/Territory | Netherlands |
City | Utrecht |
Period | 3/07/18 → 6/07/18 |
Internet address |
Keywords
- Fault maintenance trees
- Reliability
- Availability
- Maintenance
- Model checking
- Probabilistic model checking
- Statistical model checking
- Smart buildings
- HVAC