Abstract

Maintenance is essential to ensuring the dependability of a technical system. Periodic inspections, repairs, and renewals can prevent failures and extend a system’s lifespan. At the same time, maintenance incurs cost and planned downtime. It is therefore important to find a maintenance policy that balances cost and dependability. This paper presents a framework, fault maintenance trees (FMTs), integrating maintenance into the industry-standard formalism of fault trees. By translating FMTs to priced timed automata and applying statistical model checking, we can obtain system dependability metrics such as system reliability and mean time to failure, as well as costs of maintenance and failures over time, for different maintenance policies. Our framework is flexible and can be extended to include effects specific to the system being analysed. We demonstrate that our framework can be used in practice using two case studies from the railway industry: electrically insulated joints, and pneumatic compressors.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques
Subtitle of host publication7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationBerlin
PublisherSpringer Verlag
Pages151-165
Number of pages15
ISBN (Electronic)978-3-319-47166-2
ISBN (Print)978-3-319-47165-5
DOIs
StatePublished - Oct 2016
Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume9952
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Abbreviated titleISoLA 2016
CountryGreece
CityCorfu
Period10/10/1614/10/16
Internet address

Fingerprint

Model checking
Metric system
Costs
Pneumatics
Compressors
Industry
Repair
Inspection

Keywords

  • Statistical Model Checking
  • EWI-27088
  • Fault Maintenance Trees
  • IR-100740
  • Fault Trees
  • METIS-318465
  • Fault Tree Analysis

Cite this

Ruijters, E., & Stoelinga, M. (2016). Better railway engineering through statistical model checking. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I (pp. 151-165). (Lecture Notes in Computer Science; Vol. 9952). Berlin: Springer Verlag. DOI: 10.1007/978-3-319-47166-2_10

Ruijters, Enno; Stoelinga, Mariëlle / Better railway engineering through statistical model checking.

Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. Berlin : Springer Verlag, 2016. p. 151-165 (Lecture Notes in Computer Science; Vol. 9952).

Research output: Scientific - peer-reviewConference contribution

@inbook{5d97fc79492b4ed5a889bb30aa631840,
title = "Better railway engineering through statistical model checking",
abstract = "Maintenance is essential to ensuring the dependability of a technical system. Periodic inspections, repairs, and renewals can prevent failures and extend a system’s lifespan. At the same time, maintenance incurs cost and planned downtime. It is therefore important to find a maintenance policy that balances cost and dependability. This paper presents a framework, fault maintenance trees (FMTs), integrating maintenance into the industry-standard formalism of fault trees. By translating FMTs to priced timed automata and applying statistical model checking, we can obtain system dependability metrics such as system reliability and mean time to failure, as well as costs of maintenance and failures over time, for different maintenance policies. Our framework is flexible and can be extended to include effects specific to the system being analysed. We demonstrate that our framework can be used in practice using two case studies from the railway industry: electrically insulated joints, and pneumatic compressors.",
keywords = "Statistical Model Checking, EWI-27088, Fault Maintenance Trees, IR-100740, Fault Trees, METIS-318465, Fault Tree Analysis",
author = "Enno Ruijters and Mariëlle Stoelinga",
note = "eemcs-eprint-27088",
year = "2016",
month = "10",
doi = "10.1007/978-3-319-47166-2_10",
isbn = "978-3-319-47165-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "151--165",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques",
address = "Germany",

}

Ruijters, E & Stoelinga, M 2016, Better railway engineering through statistical model checking. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9952, Springer Verlag, Berlin, pp. 151-165, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, Corfu, Greece, 10-14 October. DOI: 10.1007/978-3-319-47166-2_10

Better railway engineering through statistical model checking. / Ruijters, Enno; Stoelinga, Mariëlle.

Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. Berlin : Springer Verlag, 2016. p. 151-165 (Lecture Notes in Computer Science; Vol. 9952).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Better railway engineering through statistical model checking

AU - Ruijters,Enno

AU - Stoelinga,Mariëlle

N1 - eemcs-eprint-27088

PY - 2016/10

Y1 - 2016/10

N2 - Maintenance is essential to ensuring the dependability of a technical system. Periodic inspections, repairs, and renewals can prevent failures and extend a system’s lifespan. At the same time, maintenance incurs cost and planned downtime. It is therefore important to find a maintenance policy that balances cost and dependability. This paper presents a framework, fault maintenance trees (FMTs), integrating maintenance into the industry-standard formalism of fault trees. By translating FMTs to priced timed automata and applying statistical model checking, we can obtain system dependability metrics such as system reliability and mean time to failure, as well as costs of maintenance and failures over time, for different maintenance policies. Our framework is flexible and can be extended to include effects specific to the system being analysed. We demonstrate that our framework can be used in practice using two case studies from the railway industry: electrically insulated joints, and pneumatic compressors.

AB - Maintenance is essential to ensuring the dependability of a technical system. Periodic inspections, repairs, and renewals can prevent failures and extend a system’s lifespan. At the same time, maintenance incurs cost and planned downtime. It is therefore important to find a maintenance policy that balances cost and dependability. This paper presents a framework, fault maintenance trees (FMTs), integrating maintenance into the industry-standard formalism of fault trees. By translating FMTs to priced timed automata and applying statistical model checking, we can obtain system dependability metrics such as system reliability and mean time to failure, as well as costs of maintenance and failures over time, for different maintenance policies. Our framework is flexible and can be extended to include effects specific to the system being analysed. We demonstrate that our framework can be used in practice using two case studies from the railway industry: electrically insulated joints, and pneumatic compressors.

KW - Statistical Model Checking

KW - EWI-27088

KW - Fault Maintenance Trees

KW - IR-100740

KW - Fault Trees

KW - METIS-318465

KW - Fault Tree Analysis

U2 - 10.1007/978-3-319-47166-2_10

DO - 10.1007/978-3-319-47166-2_10

M3 - Conference contribution

SN - 978-3-319-47165-5

T3 - Lecture Notes in Computer Science

SP - 151

EP - 165

BT - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

PB - Springer Verlag

ER -

Ruijters E, Stoelinga M. Better railway engineering through statistical model checking. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. Berlin: Springer Verlag. 2016. p. 151-165. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-47166-2_10