{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,12]],"date-time":"2025-07-12T22:58:28Z","timestamp":1752361108794,"version":"3.41.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T00:00:00Z","timestamp":1745280000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T00:00:00Z","timestamp":1745280000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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\u2019s 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 <jats:sc>Uppaal<\/jats:sc>\u00a0<jats:sc>Stratego<\/jats:sc> 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 a wide range of other metrics, including expected availability. We apply these techniques to the emergency shutdown system of a research nuclear reactor. In this case study, the failure probability is low, so we change the settings of <jats:sc>Uppaal<\/jats:sc>\u00a0<jats:sc>Stratego<\/jats:sc> setting to obtain reliable results about rare events. We consider both a single subsystem and the combination of two subsystems. In both situations, our methods find the optimal number of spares, minimizing cost while ensuring an expected availability of 99.96% and 99.93%, respectively.<\/jats:p>","DOI":"10.1007\/s10009-025-00791-4","type":"journal-article","created":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T15:12:39Z","timestamp":1745334759000},"page":"361-376","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Optimal spare management via statistical model checking: a case study in research reactors"],"prefix":"10.1007","volume":"27","author":[{"given":"Reza","family":"Soltani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Diamonte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milan","family":"Lopuha\u00e4-Zwakenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,4,22]]},"reference":[{"issue":"2","key":"791_CR1","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/j.ejor.2017.07.058","volume":"266","author":"Q. Hu","year":"2018","unstructured":"Hu, Q., Boylan, J.E., Chen, H., Labib, A.: OR in spare parts management: a review. Eur. J. Oper. Res. 266(2), 395\u2013414 (2018). https:\/\/doi.org\/10.1016\/j.ejor.2017.07.058","journal-title":"Eur. J. Oper. Res."},{"issue":"2","key":"791_CR2","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1016\/j.ejor.2017.03.019","volume":"262","author":"X. Zhang","year":"2017","unstructured":"Zhang, X., Zeng, J.: Joint optimization of condition-based opportunistic maintenance and spare parts provisioning policy in multiunit systems. Eur. J. Oper. Res. 262(2), 479\u2013498 (2017). https:\/\/doi.org\/10.1016\/j.ejor.2017.03.019","journal-title":"Eur. J. Oper. Res."},{"key":"791_CR3","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.cosrev.2015.03.001","volume":"15","author":"E. Ruijters","year":"2015","unstructured":"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\u201362 (2015). https:\/\/doi.org\/10.1016\/j.cosrev.2015.03.001","journal-title":"Comput. Sci. Rev."},{"key":"791_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/RAM.2018.8463074","volume-title":"2018 Annual Reliability and Maintainability Symposium (RAMS)","author":"R. Heijblom","year":"2018","unstructured":"Heijblom, R., Postma, W., Natarajan, V., Stoelinga, M.: In: 2018 Annual Reliability and Maintainability Symposium (RAMS), pp.\u00a01\u20137 (2018). https:\/\/doi.org\/10.1109\/RAM.2018.8463074"},{"key":"791_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"TACAS","author":"A. David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: In: TACAS. Lecture Notes in Computer Science, vol.\u00a09035, pp.\u00a0206\u2013211. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"key":"791_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"RV","author":"A. Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: In: RV, Lecture Notes in Computer Science, vol.\u00a06418, pp.\u00a0122\u2013135. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"key":"791_CR7","series-title":"IFAC Proceedings Volumes","doi-asserted-by":"publisher","first-page":"238","DOI":"10.3182\/20090916-3-ES-3003.00042","volume-title":"ADHS","author":"T. Chatain","year":"2009","unstructured":"Chatain, T., David, A., Larsen, K.G.: In: ADHS, IFAC Proceedings Volumes, vol.\u00a042, pp.\u00a0238\u2013243. Elsevier, Amsterdam (2009). https:\/\/doi.org\/10.3182\/20090916-3-ES-3003.00042"},{"key":"791_CR8","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-031-43681-9_12","volume-title":"International Conference on Formal Methods for Industrial Critical Systems","author":"R. Soltani","year":"2023","unstructured":"Soltani, R., Volk, M., Diamonte, L., Lopuha\u00e4-Zwakenberg, M., Stoelinga, M.: In: International Conference on Formal Methods for Industrial Critical Systems, pp.\u00a0205\u2013223. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-43681-9_12"},{"doi-asserted-by":"publisher","unstructured":"Soltani, R., Volk, M., Diamonte, L., Lopuha\u00e4-Zwakenberg, M., Stoelinga, M.: Artefact for \u201coptimal spare management via statistical model checking: a case study in research reactors\u201d (2023). https:\/\/doi.org\/10.5281\/zenodo.8199172","key":"791_CR9","DOI":"10.5281\/zenodo.8199172"},{"doi-asserted-by":"publisher","unstructured":"Zhang, S., Huang, K., Yuan, Y.: Spare parts inventory management: a literature review. Sustainability 13(5) (2021). https:\/\/doi.org\/10.3390\/su13052460","key":"791_CR10","DOI":"10.3390\/su13052460"},{"issue":"5","key":"791_CR11","doi-asserted-by":"publisher","first-page":"1629","DOI":"10.1177\/0309524X221095258","volume":"46","author":"M.I.H. Tusar","year":"2022","unstructured":"Tusar, M.I.H., Sarker, B.R.: Spare parts control strategies for offshore wind farms: a critical review and comparative study. Wind Eng. 46(5), 1629\u20131656 (2022). https:\/\/doi.org\/10.1177\/0309524X221095258","journal-title":"Wind Eng."},{"issue":"9","key":"791_CR12","doi-asserted-by":"publisher","first-page":"6695","DOI":"10.1016\/j.eswa.2010.04.037","volume":"37","author":"F. Chen","year":"2010","unstructured":"Chen, F., Chen, Y., Kuo, J.: Applying moving back-propagation neural network and moving fuzzy-neuron network to predict the requirement of critical spare parts. Expert Syst. Appl. 37(9), 6695\u20136704 (2010). https:\/\/doi.org\/10.1016\/j.eswa.2010.04.037","journal-title":"Expert Syst. Appl."},{"issue":"2","key":"791_CR13","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/j.ijpe.2007.01.007","volume":"111","author":"R.S. Gutierrez","year":"2008","unstructured":"Gutierrez, R.S., Solis, A.O., Mukhopadhyay, S.: Lumpy demand forecasting using neural networks. Int. J. Prod. Econ. 111(2), 409\u2013420 (2008). https:\/\/doi.org\/10.1016\/j.ijpe.2007.01.007. Special Section on Sustainable Supply Chain","journal-title":"Int. J. Prod. Econ."},{"issue":"1","key":"791_CR14","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1016\/j.ijpe.2013.01.009","volume":"143","author":"N. Kourentzes","year":"2013","unstructured":"Kourentzes, N.: Intermittent demand forecasts with neural networks. Int. J. Prod. Econ. 143(1), 198\u2013206 (2013). https:\/\/doi.org\/10.1016\/j.ijpe.2013.01.009","journal-title":"Int. J. Prod. Econ."},{"issue":"2","key":"791_CR15","doi-asserted-by":"publisher","first-page":"1144","DOI":"10.1016\/j.eswa.2006.12.003","volume":"34","author":"S.G. Li","year":"2008","unstructured":"Li, S.G., Kuo, X.: The inventory management system for automobile spare parts in a central warehouse. Expert Syst. Appl. 34(2), 1144\u20131153 (2008). https:\/\/doi.org\/10.1016\/j.eswa.2006.12.003","journal-title":"Expert Syst. Appl."},{"issue":"6","key":"791_CR16","doi-asserted-by":"publisher","first-page":"2660","DOI":"10.1016\/j.eswa.2013.11.007","volume":"41","author":"P. Wu","year":"2014","unstructured":"Wu, P., Hung, Y., Lin, Z.: Intelligent forecasting system based on integration of electromagnetism-like mechanism and fuzzy neural network. Expert Syst. Appl. 41(6), 2660\u20132677 (2014). https:\/\/doi.org\/10.1016\/j.eswa.2013.11.007","journal-title":"Expert Syst. Appl."},{"key":"791_CR17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2021.107512","volume":"210","author":"M. Zheng","year":"2021","unstructured":"Zheng, M., Ye, H., Wang, D., Pan, E.: Joint optimization of condition-based maintenance and spare parts orders for multi-unit systems with dual sourcing. Reliab. Eng. Syst. Saf. 210, 107512 (2021). https:\/\/doi.org\/10.1016\/j.ress.2021.107512","journal-title":"Reliab. Eng. Syst. Saf."},{"unstructured":"Soltani, R., Kang, E.Y., Mena, J.E.H.: Verification and optimization of cyber-physical systems: Preprint for FedCSIS (2021). arXiv:2109.01574. arXiv preprint","key":"791_CR18"},{"key":"791_CR19","doi-asserted-by":"publisher","first-page":"205","DOI":"10.15439\/2021F125","volume-title":"FedCSIS (Position Papers)","author":"R. Soltani","year":"2021","unstructured":"Soltani, R., Kang, E.Y., Mena, J.E.H.: In: FedCSIS (Position Papers), pp.\u00a0205\u2013210 (2021). https:\/\/doi.org\/10.15439\/2021F125"},{"key":"791_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-22975-1_11","volume-title":"FORMATS","author":"R. Kumar","year":"2015","unstructured":"Kumar, R., Ruijters, E., Stoelinga, M.: In: FORMATS. Lecture Notes in Computer Science, vol.\u00a09268, pp.\u00a0156\u2013171. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-22975-1_11"},{"key":"791_CR21","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/HASE.2017.12","volume-title":"HASE","author":"R. Kumar","year":"2017","unstructured":"Kumar, R., Stoelinga, M.: In: HASE, pp.\u00a025\u201332. IEEE Comput. Soc., Los Alamitos (2017). https:\/\/doi.org\/10.1109\/HASE.2017.12"},{"key":"791_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"FORMATS","author":"A. David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: In: FORMATS. Lecture Notes in Computer Science, vol.\u00a06919, pp.\u00a080\u201396. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_7"},{"key":"791_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-47166-2_10","volume-title":"ISoLA (1)","author":"E. Ruijters","year":"2016","unstructured":"Ruijters, E., Stoelinga, M.: In: ISoLA (1). Lecture Notes in Computer Science, vol.\u00a09952, pp.\u00a0151\u2013165 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_10"},{"key":"791_CR24","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1109\/ELMAR52657.2021.9550961","volume-title":"2021 International Symposium ELMAR","author":"S.C. Jepsen","year":"2021","unstructured":"Jepsen, S.C., Worm, T., Johansen, A., Lazarova-Molnar, S., Kj\u00e6rgaard, M.B., Kang, E.Y., Friederich, J., Heredia Mena, J.E., Soltani, R., S\u00f8rensen, S.L., Hjort Schwee, J.: In: 2021 International Symposium ELMAR, pp.\u00a0143\u2013150 (2021). https:\/\/doi.org\/10.1109\/ELMAR52657.2021.9550961"},{"key":"791_CR25","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1016\/j.eswa.2017.01.058","volume":"77","author":"S. Kabir","year":"2017","unstructured":"Kabir, S.: An overview of fault tree analysis and its application in model based dependability analysis. Expert Syst. Appl. 77, 114\u2013135 (2017). https:\/\/doi.org\/10.1016\/j.eswa.2017.01.058","journal-title":"Expert Syst. Appl."},{"key":"791_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-59042-0_76","volume-title":"STACS","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: In: STACS. Lecture Notes in Computer Science, vol.\u00a0900, pp.\u00a0229\u2013242. Springer, Berlin (1995). https:\/\/doi.org\/10.1007\/3-540-59042-0_76"},{"key":"791_CR27","series-title":"EPTCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.85.1","volume-title":"QAPL","author":"P.E. Bulychev","year":"2012","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: In: QAPL, EPTCS, vol.\u00a085, pp.\u00a01\u201316 (2012). https:\/\/doi.org\/10.4204\/EPTCS.85.1"},{"key":"791_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"CAV","author":"G. Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: In: CAV. Lecture Notes in Computer Science, vol.\u00a04590, pp.\u00a0121\u2013125. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14"},{"key":"791_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"ATVA","author":"A. David","year":"2014","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8rensen, M.G., Taankvist, J.H.: In: ATVA. Lecture Notes in Computer Science, vol.\u00a08837, pp.\u00a0129\u2013145. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_10"},{"key":"791_CR30","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1109\/DSN.2007.37","volume-title":"DSN","author":"H. Boudali","year":"2007","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: In: DSN, pp.\u00a0708\u2013717. IEEE Comput. Soc., Los Alamitos (2007). https:\/\/doi.org\/10.1109\/DSN.2007.37"},{"key":"791_CR31","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/DSN.2016.67","volume-title":"DSN","author":"E. Ruijters","year":"2016","unstructured":"Ruijters, E., Guck, D., van Noort, M., Stoelinga, M.: In: DSN, pp.\u00a0662\u2013669. IEEE Comput. Soc., Los Alamitos (2016). https:\/\/doi.org\/10.1109\/DSN.2016.67"},{"unstructured":"UPPAAL requirements specification language. https:\/\/docs.uppaal.org\/language-reference\/requirements-specification\/. Accessed: 2023-05-26","key":"791_CR32"},{"key":"791_CR33","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-031-68606-1_14","volume-title":"Computer Safety, Reliability, and Security","author":"R. Soltani","year":"2024","unstructured":"Soltani, R., Lopuha\u00e4-Zwakenberg, M., Stoelinga, M.: In: Ceccarelli, A., Trapp, M., Bondavalli, A., Bitsch, F. (eds.) Computer Safety, Reliability, and Security, pp.\u00a0218\u2013232. Springer, Cham (2024)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00791-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-025-00791-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00791-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T10:14:39Z","timestamp":1750932879000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-025-00791-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,22]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["791"],"URL":"https:\/\/doi.org\/10.1007\/s10009-025-00791-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2025,4,22]]},"assertion":[{"value":"4 April 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 April 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}