Skip to main content
SpringerLink
Log in

Modelling Smart Buildings Using Fault Maintenance Trees

  • Conference paper
  • First Online:
Book cover Computer Performance Engineering (EPEW 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11178))

Included in the following conference series:

  • 484 Accesses

Abstract

Increasingly many industrial spheres are enforced by law to satisfy strict RAMS requirements—reliability, availability, maintainability, and safety. Applied to Fault Maintenance Trees (FMTs), formal methods offer flexible and trustworthy techniques to quantify the resilience of (abstract models of) systems. However, the estimated metrics are relevant only as far as the model reflects the actual system: Refining an abstract model to reduce the gap with reality is crucial for the usefulness of the results. In this work, we take a practical approach at the challenge by studying a Heating, Ventilation and Air-Conditioning unit (HVAC), ubiquitous in smart buildings. Using probabilistic and statistical model checking, we assess RAMS metrics of a basic fault maintenance tree HVAC model. We then implement four modifications augmenting the expressivity of the FMT model, and show that reliability, availability, expected number of failures, and costs, can vary by orders of magnitude depending on involved modelling details.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Support for reward analysis on PTA with PRISM is ongoing research, see Sect. 4.

  2. 2.

    Higher redundancies lead to rare failures that hinder SMC analyses, see Sect. 4.

  3. 3.

    Notice that a valve can be replaced in hours, whereas all time horizons are in years.

References

  1. Aven, T., Jensen, U. (eds.): Maintenance optimization. Stochastic Models in Reliability, pp. 169–211. Springer, New York (1999). https://doi.org/10.1007/978-0-387-22593-7_5

  2. ASHRAE: HVAC systems and equipment. American Society of Heating, Refrigerating, and Air Conditioning Engineers, Atlanta, GA (1996)

    Google Scholar 

  3. Au-Yong, C.P., Ali, A.S., Ahmad, F.: Enhancing building maintenance cost performance with proper management of spare parts. JQME 22(1), 51–61 (2016)

    Article  Google Scholar 

  4. Barlow, R.E., Proschan, F.: Mathematical theory of reliability. Science 148(3674), 1208–1209 (1965)

    Article  Google Scholar 

  5. Cauchi, N., Hoque, K.A., Abate, A., Stoelinga, M.: Efficient probabilistic model checking of smart building maintenance using fault maintenance trees. In: BuildSys (2017)

    Google Scholar 

  6. Cauchi, N., Macek, K., Abate, A.: Model-based predictive maintenance inbuilding automation systems with user discomfort. Energy 138(Suppl. C), 306–315 (2017)

    Article  Google Scholar 

  7. Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 244–263 (1986)

    Article  Google Scholar 

  8. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  9. David, A., Larsen, K., Legay, A., Mikučionis, M., Poulsen, D.: Uppaal SMC tutorial. Intl. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)

    Article  Google Scholar 

  10. David, A., Larry, S.: The least variable phase type distribution is Erlang. Communications in statistics. Stoch. Models 3(3), 467–473 (1987)

    Article  MathSciNet  Google Scholar 

  11. Dugan, J.B., Bavuso, S.J., Boyd, M.A.: Fault trees and sequence dependencies. In: RAMS, pp. 286–293 (1990)

    Google Scholar 

  12. Faisal, I., Mahmoud, M.: Risk-based maintenance (RBM): a quantitative approach for maintenance/inspection scheduling and planning. J. Loss Prev. Process Ind. 16(6), 561–573 (2003)

    Google Scholar 

  13. Guck, D., Spel, J., Stoelinga, M.: DFTCalc: reliability centered maintenance via fault tree analysis (tool paper). In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 304–311. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_19

    Chapter  Google Scholar 

  14. Junges, S., Guck, D., Katoen, J.P., Stoelinga, M.: Uncovering dynamic fault trees. In: DSN, pp. 299–310. IEEE, June 2016

    Google Scholar 

  15. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking: advances and applications. In: Drechsler, R. (ed.) Formal System Verification, pp. 73–121. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-57685-5_3

    Chapter  Google Scholar 

  16. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  17. Nicolai, R.P., Dekker, R.: Optimal maintenance of multi-component systems: a review. In: Kobbacy, K.A.H., Murthy, D.N.P. (eds.) Complex System Maintenance Handbook, pp. 263–286. Springer, Heidelberg (2008). https://doi.org/10.1007/978-1-84800-011-7_11

    Chapter  Google Scholar 

  18. Rubino, G., Tuffin, B. (eds.): Rare Event Simulation Using Monte Carlo Methods. Wiley, Hoboken (2009)

    MATH  Google Scholar 

  19. Ruijters, E., Guck, D., Drolenga, P., Peters, M., Stoelinga, M.: Maintenance analysis and optimization via statistical model checking. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 331–347. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43425-4_22

    Chapter  Google Scholar 

  20. Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29–62 (2015)

    Article  MathSciNet  Google Scholar 

  21. Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault tree handbook. Technical report, U.S. Nuclear Regulatory Commission, Washington DC (1981)

    Google Scholar 

  22. Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Inform. 14(1), 370–379 (2018)

    Article  Google Scholar 

  23. Wang, D., Tsui, K.L.: Statistical modeling of bearing degradation signals. IEEE Trans. Reliab. 66(4), 1331–1344 (2017)

    Article  Google Scholar 

  24. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_17

    Chapter  MATH  Google Scholar 

Download references

Acknowledgements

This work is partially supported by the Alan Turing Institute, UK; Malta’s ENDEAVOUR Scholarships Scheme; and the NWO SEQUOIA project.

Author information

Authors and Affiliations

  1. Formal Methods and Tools Group, University of Twente, Enschede, The Netherlands

    Carlos E. Budde, Arnaud van Harmelen & Mariëlle Stoelinga

  2. Department of Computer Science, University of Oxford, Oxford, UK

    Alessandro Abate & Nathalie Cauchi

  3. Department of Software Science, Radboud University, Nijmegen, The Netherlands

    Mariëlle Stoelinga

  4. Department of Electrical Engineering and Computer Science, University of Missouri, Columbia, USA

    Khaza Anuarul Hoque

Authors
  1. Alessandro Abate
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carlos E. Budde
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nathalie Cauchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Arnaud van Harmelen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Khaza Anuarul Hoque
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Mariëlle Stoelinga
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Carlos E. Budde .

Editor information

Editors and Affiliations

  1. eScience Center, Amsterdam, The Netherlands

    Rena Bakhshi

  2. University Paris-Saclay, Gif-sur-Yvette, France

    Paolo Ballarini

  3. Université Paris-Est Créteil, Créteil, France

    Benoît Barbot

  4. Telecom SudParis, Evry, France

    Hind Castel-Taleb

  5. Westfälische Wilhelms Universität Münster, Münster, Germany

    Anne Remke

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Abate, A., Budde, C.E., Cauchi, N., van Harmelen, A., Hoque, K.A., Stoelinga, M. (2018). Modelling Smart Buildings Using Fault Maintenance Trees. In: Bakhshi, R., Ballarini, P., Barbot, B., Castel-Taleb, H., Remke, A. (eds) Computer Performance Engineering. EPEW 2018. Lecture Notes in Computer Science(), vol 11178. Springer, Cham. https://doi.org/10.1007/978-3-030-02227-3_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02227-3_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02226-6

  • Online ISBN: 978-3-030-02227-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation