Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors

Reza Soltani; Matthias Volk; Leonardo Diamonte; Milan Lopuhaä-Zwakenberg; Mariëlle Stoelinga

doi:10.1007/978-3-031-43681-9_12

Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors

Reza Soltani^*, Matthias Volk, Leonardo Diamonte, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

50 Downloads (Pure)

Abstract

Systematic spare management is important to optimize the twin goals of high reliability and low costs. However, existing approaches to spare management do not incorporate a detailed analysis of the effect on the absence of spares on the system’s reliability. In this work, we combine fault tree analysis with statistical model checking to model spare part management as a stochastic priced timed game automaton (SPTGA). We use UPPAAL STRATEGO to find the number of spares that minimizes the total costs due to downtime and spare purchasing; the resulting SPTGA model can then additionally be analyzed according to other metrics like expected availability. We apply these techniques to the emergency shutdown system of a research nuclear reactor. Our methods find the optimal spare management for a subsystem in a matter of minutes, minimizing cost while ensuring an expected availability of 99.96%.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings
Editors	Alessandro Cimatti, Laura Titolo
Place of Publication	Cham, Switzerland
Publisher	Springer Nature
Pages	205-223
Number of pages	19
ISBN (Electronic)	978-3-031-43681-9
ISBN (Print)	978-3-031-43680-2
DOIs	https://doi.org/10.1007/978-3-031-43681-9_12
Publication status	Published - 17 Sept 2023
Event	28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023 - Antwerp, Belgium Duration: 20 Sept 2023 → 22 Sept 2023 Conference number: 28

Publication series

Name	Lecture notes in computer science
Publisher	Springer Nature
Volume	14290
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023
Abbreviated title	FMICS 2023
Country/Territory	Belgium
City	Antwerp
Period	20/09/23 → 22/09/23

Keywords

2023 OA procedure

Access to Document

10.1007/978-3-031-43681-9_12

ArticleFinal published version, 1.4 MBLicence: Taverne

Artefact for "Optimal spare management via statistical model checking: A case study in research reactors"
Soltani, R. (Creator), Volk, M. (Creator), Diamonte, L. A. (Creator), Lopuhaä - Zwakenberg, M. A. (Creator) & Stoelinga, M. I. A. (Creator), Zenodo, 31 Jul 2023
DOI: 10.5281/zenodo.8199172
Dataset

Cite this

Soltani, R., Volk, M., Diamonte, L., Lopuhaä-Zwakenberg, M., & Stoelinga, M. (2023). Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors. In A. Cimatti, & L. Titolo (Eds.), Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings (pp. 205-223). (Lecture notes in computer science; Vol. 14290). Springer Nature. https://doi.org/10.1007/978-3-031-43681-9_12

Soltani, Reza ; Volk, Matthias ; Diamonte, Leonardo et al. / Optimal Spare Management via Statistical Model Checking : A Case Study in Research Reactors. Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. editor / Alessandro Cimatti ; Laura Titolo. Cham, Switzerland : Springer Nature, 2023. pp. 205-223 (Lecture notes in computer science).

@inproceedings{b768b2da1a884a22a4604f328d8116aa,

title = "Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors",

abstract = "Systematic spare management is important to optimize the twin goals of high reliability and low costs. However, existing approaches to spare management do not incorporate a detailed analysis of the effect on the absence of spares on the system{\textquoteright}s reliability. In this work, we combine fault tree analysis with statistical model checking to model spare part management as a stochastic priced timed game automaton (SPTGA). We use UPPAAL STRATEGO to find the number of spares that minimizes the total costs due to downtime and spare purchasing; the resulting SPTGA model can then additionally be analyzed according to other metrics like expected availability. We apply these techniques to the emergency shutdown system of a research nuclear reactor. Our methods find the optimal spare management for a subsystem in a matter of minutes, minimizing cost while ensuring an expected availability of 99.96%.",

keywords = "2023 OA procedure",

author = "Reza Soltani and Matthias Volk and Leonardo Diamonte and Milan Lopuha{\"a}-Zwakenberg and Mari{\"e}lle Stoelinga",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023, FMICS 2023 ; Conference date: 20-09-2023 Through 22-09-2023",

year = "2023",

month = sep,

day = "17",

doi = "10.1007/978-3-031-43681-9_12",

language = "English",

isbn = "978-3-031-43680-2",

series = "Lecture notes in computer science",

publisher = "Springer Nature",

pages = "205--223",

editor = "Alessandro Cimatti and Laura Titolo",

booktitle = "Formal Methods for Industrial Critical Systems",

address = "Switzerland",

}

Soltani, R, Volk, M, Diamonte, L, Lopuhaä-Zwakenberg, M & Stoelinga, M 2023, Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors. in A Cimatti & L Titolo (eds), Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. Lecture notes in computer science, vol. 14290, Springer Nature, Cham, Switzerland, pp. 205-223, 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023, Antwerp, Belgium, 20/09/23. https://doi.org/10.1007/978-3-031-43681-9_12

Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors. / Soltani, Reza; Volk, Matthias; Diamonte, Leonardo et al.
Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. ed. / Alessandro Cimatti; Laura Titolo. Cham, Switzerland: Springer Nature, 2023. p. 205-223 (Lecture notes in computer science; Vol. 14290).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Optimal Spare Management via Statistical Model Checking

T2 - 28th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2023

AU - Soltani, Reza

AU - Volk, Matthias

AU - Diamonte, Leonardo

AU - Lopuhaä-Zwakenberg, Milan

AU - Stoelinga, Mariëlle

N1 - Conference code: 28

PY - 2023/9/17

Y1 - 2023/9/17

N2 - Systematic spare management is important to optimize the twin goals of high reliability and low costs. However, existing approaches to spare management do not incorporate a detailed analysis of the effect on the absence of spares on the system’s reliability. In this work, we combine fault tree analysis with statistical model checking to model spare part management as a stochastic priced timed game automaton (SPTGA). We use UPPAAL STRATEGO to find the number of spares that minimizes the total costs due to downtime and spare purchasing; the resulting SPTGA model can then additionally be analyzed according to other metrics like expected availability. We apply these techniques to the emergency shutdown system of a research nuclear reactor. Our methods find the optimal spare management for a subsystem in a matter of minutes, minimizing cost while ensuring an expected availability of 99.96%.

AB - Systematic spare management is important to optimize the twin goals of high reliability and low costs. However, existing approaches to spare management do not incorporate a detailed analysis of the effect on the absence of spares on the system’s reliability. In this work, we combine fault tree analysis with statistical model checking to model spare part management as a stochastic priced timed game automaton (SPTGA). We use UPPAAL STRATEGO to find the number of spares that minimizes the total costs due to downtime and spare purchasing; the resulting SPTGA model can then additionally be analyzed according to other metrics like expected availability. We apply these techniques to the emergency shutdown system of a research nuclear reactor. Our methods find the optimal spare management for a subsystem in a matter of minutes, minimizing cost while ensuring an expected availability of 99.96%.

KW - 2023 OA procedure

U2 - 10.1007/978-3-031-43681-9_12

DO - 10.1007/978-3-031-43681-9_12

M3 - Conference contribution

SN - 978-3-031-43680-2

T3 - Lecture notes in computer science

SP - 205

EP - 223

BT - Formal Methods for Industrial Critical Systems

A2 - Cimatti, Alessandro

A2 - Titolo, Laura

PB - Springer Nature

CY - Cham, Switzerland

Y2 - 20 September 2023 through 22 September 2023

ER -

Soltani R, Volk M, Diamonte L, Lopuhaä-Zwakenberg M , Stoelinga M. Optimal Spare Management via Statistical Model Checking: A Case Study in Research Reactors. In Cimatti A, Titolo L, editors, Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings. Cham, Switzerland: Springer Nature. 2023. p. 205-223. (Lecture notes in computer science). doi: 10.1007/978-3-031-43681-9_12