{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T21:25:24Z","timestamp":1768425924887,"version":"3.49.0"},"reference-count":77,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T00:00:00Z","timestamp":1744675200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T00:00:00Z","timestamp":1744675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Deutsches Zentrum f\u00fcr Luft- und Raumfahrt e.V. (DLR)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Ensuring the correct and safe behavior of a spacecraft is a main objective in space-system design. Since spacecraft consist of highly complex and tightly integrated components developed by large teams of engineers from various different disciplines, this is a challenging task. Increasingly, formal verification methods such as model checking are applied to establish the correctness of safety-critical parts or subsystems. Generally, the often limited scalability of model checking due to the state-space explosion problem hinders the wide-spread adoption of this technique. In this paper, we systematically examine the scalability of model checking for verifying behavioral models that arise within early space-system design phases. For this, we created a representative model for the mode management of a satellite that can be scaled in terms of its size and the complexity of interactions between system components. The model can be transformed into the input languages of various model-checking tools, which enables a comparative study of various model-checking algorithms and also facilitates analyzing the impact of different communication schemes on the scalability. The evaluation shows promising results regarding the applicability of model checking within the spacecraft design process.<\/jats:p>","DOI":"10.1007\/s10270-025-01281-6","type":"journal-article","created":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T01:22:19Z","timestamp":1744680139000},"page":"1825-1846","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Model checking of spacecraft operational designs: a scalability analysis"],"prefix":"10.1007","volume":"24","author":[{"given":"Philipp","family":"Chrszon","sequence":"first","affiliation":[]},{"given":"Paulina","family":"Maurer","sequence":"additional","affiliation":[]},{"given":"George","family":"Saleip","sequence":"additional","affiliation":[]},{"given":"Sascha","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Philipp M.","family":"Fischer","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Gerndt","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Felderer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,4,15]]},"reference":[{"key":"1281_CR1","doi-asserted-by":"crossref","unstructured":"Davis, J.A., Clark, M.A., Cofer, D.D., Fifarek, A.,Hinchman, J., Hoffman, J.A., Hulbert, B.W., Miller, S.P., Wagner, L.G.: Study on the barriers to the industrial adoption of formal methods. In: Pecheur, C., Dierkes, M. (eds.) Formal Methods for Industrial Critical Systems - 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings, series. Lecture Notes in Computer Science, vol. 8187, pp. 63\u201377. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-41010-9_5"},{"issue":"6","key":"1281_CR2","doi-asserted-by":"publisher","first-page":"4473","DOI":"10.1007\/s10664-020-09836-5","volume":"25","author":"M Gleirscher","year":"2020","unstructured":"Gleirscher, M., Marmsoler, D.: Formal methods in dependable systems engineering: a survey of professionals from Europe and North America. Empir. Softw. Eng. 25(6), 4473\u20134546 (2020)","journal-title":"Empir. Softw. Eng."},{"key":"1281_CR3","doi-asserted-by":"crossref","unstructured":"Chien, S.A.: Formal methods for trusted space autonomy: Boon or bane? In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings, series. Lecture Notes in Computer Science, vol. 13260, pp. 3\u201313. Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-06773-0_1"},{"key":"1281_CR4","doi-asserted-by":"crossref","unstructured":"Chrszon, P., Maurer, P., Saleip, G., M\u00fcller, S., Fischer, P.M., Gerndt, A., Felderer, M.: Applicability of model checking for verifying spacecraft operational designs. In: 26th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2023, V\u00e4ster\u00e5s, Sweden, October 1-6, 2023, pp. 206\u2013216. IEEE (2023)","DOI":"10.1109\/MODELS58315.2023.00011"},{"key":"1281_CR5","unstructured":"Secretariat, E.C.S.S.: ECSS-M-ST-10C: Space project management\u2014project planning and implementation. ESA-ESTEC Requirements and Standards Division, Noordwijk, Netherlands, Standard (2009)"},{"issue":"1","key":"1281_CR6","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1177\/1063293X17734592","volume":"26","author":"PM Fischer","year":"2018","unstructured":"Fischer, P.M., Deshmukh, M., Maiwald, V., Quantius, D., Gomez, A.M., Gerndt, A.: Conceptual data model: a foundation for successful concurrent engineering. Concurr. Eng. Res. Appl. 26(1), 55\u201376 (2018)","journal-title":"Concurr. Eng. Res. Appl."},{"key":"1281_CR7","unstructured":"DLR. Virtual Satellite. Available: https:\/\/github.com\/virtualsatellite\/VirtualSatellite4-Core (2023)"},{"key":"1281_CR8","unstructured":"Jahnke, S.S., Gomez, A.M., Fischer, P.M., Lange, C.: Concurrent engineering in later project phases: current methods and future demands. In: 69th International Astronautical Congress (IAC), 10. Available: https:\/\/elib.dlr.de\/121731\/ (2018)"},{"key":"1281_CR9","doi-asserted-by":"crossref","unstructured":"D. Quantius, H. Wessel, P. M. Fischer, D. Peters.: Progression visualisation of mass parameters during a concurrent engineering study. In: Luo, Y. (ed.) Cooperative Design, Visualization, and Engineering\u201419th International Conference, CDVE: Virtual Event, September 25\u201328, 2022, Proceedings, Series. Lecture Notes in Computer Science, vol. 13492, pp. 13\u201320. Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-16538-2_2"},{"key":"1281_CR10","unstructured":"Secretariat, E.C.S.S.: ECSS-E-TM-10-21A: Space engineering\u2014system modeling and simulation. ESA-ESTEC Requirements and Standards Division, Noordwijk. Tech. Rep, Netherlands (2010)"},{"key":"1281_CR11","unstructured":"Fischer, P.M., L\u00fcdtke, D., Schaus, V., Maibaum, O., Gerndt, A.: Formal verification in early mission planning. In: Simulation and EGSE facilities for Space Programmes. Available: https:\/\/elib.dlr.de\/119907\/ (2012)"},{"key":"1281_CR12","doi-asserted-by":"crossref","unstructured":"Fischer, P.M., Ludtke, D., Schaus, V., Gerndt, A.: A formal method for early spacecraft design verification. In: 2013 IEEE Aerospace Conference, pp. 1\u20138 (2013)","DOI":"10.1109\/AERO.2013.6496878"},{"key":"1281_CR13","doi-asserted-by":"crossref","unstructured":"Schaus, V., Fischer, P.M., Ludtke, D., Tiede, M., Gerndt, A.: A Continuous Verification Process in Concurrent Engineering (2013)","DOI":"10.2514\/6.2013-5429"},{"key":"1281_CR14","unstructured":"Fischer, P.M., Deshmukh, M., Koch, A., Mischke, R., Gomez, A.M., Schreiber, A., Gerndt, A.: Enabling a conceptual data model and workflow integration environment for concurrent launch vehicle analysis. In: 69th International Astronautical Congress (IAC). https:\/\/elib.dlr.de\/122158\/ (2018)"},{"key":"1281_CR15","unstructured":"Fischer, P., Eisenmann, H., Fuchs, J.: Functional verification by simulation based on preliminary system design data. In: 6th International Workshop on Systems and Concurrent Engineering for Space Applications (SECESA), pp. 8\u201310 (2014)"},{"key":"1281_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs, Workshop, Yorktown Heights, New York, USA,: Series. Lecture Notes in Computer Science, vol. 131, pp. 52\u201371. Springer, Berlin (1981)","DOI":"10.1007\/BFb0025774"},{"key":"1281_CR17","doi-asserted-by":"crossref","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, Series. Lecture Notes in Computer Science, vol. 137, pp. 337\u2013351. Springer, Berlin (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"7","key":"1281_CR18","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"1281_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1281_CR20","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1281_CR21","volume-title":"Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd edn. MIT Press, Cambridge (2018)","edition":"2"},{"key":"1281_CR22","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21-23 October 1985. 0.5em minus, pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"1","key":"1281_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"1281_CR24","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P., Wong-Toi, H.: HYTECH: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 110\u2013122 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1281_CR25","doi-asserted-by":"crossref","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Series. Lecture Notes in Computer Science, vol. 6806, pp. 379\u2013395. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"issue":"4","key":"1281_CR26","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Formal Methods Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"1281_CR27","doi-asserted-by":"crossref","unstructured":"D.A. Peled.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) Computer Aided Verification, 5th International Conference, CAV \u201993, Elounda, Greece, June 28 - July 1: Proceedings, Series. Lecture Notes in Computer Science, vol. 697, pp. 409\u2013423. Springer, Berlin (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"1281_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems\u2014Conference proceedings, Colle-sur-Loup (near Nice), France, 8\u201319: Series. NATO ASI Series, vol. 13, pp. 123\u2013144. Springer, Berlin (1984)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"1281_CR29","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: methodology and case studies. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, 10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28\u2014July 2, 1998, Proceedings, Series. Lecture Notes in Computer Science, vol. 1427, pp. 440\u2013451. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028765"},{"issue":"1\/2","key":"1281_CR30","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1\/2), 77\u2013104 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"1281_CR31","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS \u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, March 22\u201328: Proceedings, Series. Lecture Notes in Computer Science, vol. 1579, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"1281_CR32","doi-asserted-by":"crossref","unstructured":"Williams, P.F., Biere, A., Clarke, E.M., Gupta, A.: Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, Series. Lecture Notes in Computer Science, vol. 1855, pp. 124\u2013138. Springer, Berlin (2000)","DOI":"10.1007\/10722167_13"},{"issue":"2","key":"1281_CR33","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"1281_CR34","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"8","key":"1281_CR35","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"1281_CR36","volume-title":"Onboard Computers, Onboard Software and Satellite Operations: An Introduction","author":"J Eickhoff","year":"2011","unstructured":"Eickhoff, J.: Onboard Computers, Onboard Software and Satellite Operations: An Introduction. Springer, Berlin (2011)"},{"issue":"3","key":"1281_CR37","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"1281_CR38","unstructured":"Rey, J.: Modeling with vsee: aefinition of guidelines and exploitation of the models. Available: https:\/\/www.vsd-project.org\/download\/documents\/YGT%20final%20report%20Rey%20V2.pdf"},{"issue":"5","key":"1281_CR39","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1281_CR40","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, Series. Lecture Notes in Computer Science, vol. 2404, pp. 359\u2013364. Springer, Berlin (2002),","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1281_CR41","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Series. Lecture Notes in Computer Science, vol. 6806, pp. 585\u2013591. Springer, Berlin (2011)"},{"issue":"4","key":"1281_CR42","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"1281_CR43","doi-asserted-by":"publisher","first-page":"381","DOI":"10.3390\/software1040017","volume":"1","author":"MH ter Beek","year":"2022","unstructured":"ter Beek, M.H., Ferrari, A.: Empirical formal methods: guidelines for performing empirical studies on formal methods. Software 1(4), 381\u2013416 (2022)","journal-title":"Software"},{"key":"1281_CR44","doi-asserted-by":"publisher","unstructured":"Chrszon, P.: Model Checking of Spacecraft Operational Designs: A Scalability Analysis - Artifac, (2024). https:\/\/doi.org\/10.5281\/zenodo.13998669","DOI":"10.5281\/zenodo.13998669"},{"key":"1281_CR45","unstructured":"Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011)"},{"issue":"1","key":"1281_CR46","doi-asserted-by":"publisher","first-page":"1018","DOI":"10.1109\/JSYST.2018.2793665","volume":"13","author":"V Nardone","year":"2019","unstructured":"Nardone, V., Santone, A., Tipaldi, M., Liuzza, D., Glielmo, L.: Model checking techniques applied to satellite operational mode management. IEEE Syst. J. 13(1), 1018\u20131029 (2019)","journal-title":"IEEE Syst. J."},{"issue":"2","key":"1281_CR47","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10009-017-0456-3","volume":"20","author":"J Klein","year":"2018","unstructured":"Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Kl\u00fcppelholz, S., M\u00e4rcker, S., M\u00fcller, D.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic B\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 20(2), 179\u2013194 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1281_CR48","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, E., Liu, S., Liu, Y., Choppy, C., Sun, J., Dong, J.S.: Formalizing UML state machines for automated verification-a survey. ACM Comput. Surv. 55 (2023)","DOI":"10.1145\/3579821"},{"key":"1281_CR49","unstructured":"Fecher, H., Kyas, M., Sch\u00e4nborn, J.: Semantic issues in UML 2.0 state machines. Christian-Albrechts-Universit\u00f6t Kiel, Technical Representative (2005)"},{"key":"1281_CR50","doi-asserted-by":"crossref","unstructured":"Liu, S., Liu, Y., Andr\u00e9, \u00c9., Choppy, C., Sun, J., Wadhwa, B., Dong, J.S.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings, Series. Lecture Notes in Computer Science, vol. 7940, pp. 331\u2013346. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38613-8_23"},{"key":"1281_CR51","unstructured":"Varr\u00f3, D.: A formal semantics of UML statecharts by model transition systems. In: Corradini, A., Ehrig, H., Kreowski, H., Rozenberg, G. (eds.) Graph Transformation, First International Conference, ICGT 2002, Barcelona, Spain, October 7-12, 2002, Proceedings, Series. Lecture Notes in Computer Science, vol. 2505, pp. 378\u2013392. Springer, Berlin (2002)"},{"issue":"2","key":"1281_CR52","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s10270-015-0484-y","volume":"16","author":"K Zurowska","year":"2017","unstructured":"Zurowska, K., Dingel, J.: Language-specific model checking of UML-RT models. Softw. Syst. Model. 16(2), 393\u2013415 (2017)","journal-title":"Softw. Syst. Model."},{"issue":"6","key":"1281_CR53","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects Comput. 11(6), 637\u2013664 (1999)","journal-title":"Formal Aspects Comput."},{"issue":"6","key":"1281_CR54","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1002\/sys.21679","volume":"26","author":"B Horv\u00e1th","year":"2023","unstructured":"Horv\u00e1th, B., Moln\u00e1r, V., Graics, B., Hajdu, \u00c1., R\u00e1th, I., Horv\u00e1th, \u00c1., Karban, R., Trancho, G., Micskei, Z.: Pragmatic verification and validation of industrial executable SysML models. Syst. Eng. 26(6), 693\u2013714 (2023)","journal-title":"Syst. Eng."},{"issue":"6","key":"1281_CR55","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/s10270-020-00806-5","volume":"19","author":"B Graics","year":"2020","unstructured":"Graics, B., Moln\u00e1r, V., V\u00f6r\u00f6s, A., Majzik, I., Varr\u00f3, D.: Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw. Syst. Model. 19(6), 1483\u20131517 (2020)","journal-title":"Softw. Syst. Model."},{"key":"1281_CR56","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA. IEEE Computer Society, pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"1281_CR57","doi-asserted-by":"crossref","unstructured":"T\u00f3th, T., Hajdu, \u00c1., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I., Theta: a framework for abstraction refinement-based model checking. In: Stewart, D., Weissenbacher, G. (eds.) Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2\u20136, 2017, pp. 176\u2013179. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"1281_CR58","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl, M., Leue, S., Singh, H.: \u201cFrom SysML to model checkers via model transformation,\u201d in Model Checking Software - 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018, Proceedings, ser. Lecture Notes in Computer Science, M.\u00a0Gallardo and P.\u00a0Merino, Eds., vol. 10869. Springer, (2018), pp. 255\u2013274","DOI":"10.1007\/978-3-319-94111-0_15"},{"key":"1281_CR59","doi-asserted-by":"crossref","unstructured":"Dubrovin, J., Junttila, T.A.: Symbolic model checking of hierarchical UML state machines. In: Billington, J., Duan, Z., Koutny, M. (eds.) 8th International Conference on Application of Concurrency to System Design (ACSD 2008), Xi\u2019an, China, June 23-27, 2008, pp. 108\u2013117. IEEE (2008)","DOI":"10.1109\/ACSD.2008.4574602"},{"key":"1281_CR60","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez, M.E.B., Barrio-Sol\u00f3rzano, M., Quintero, C.E.C., de\u00a0la Fuente, P.: UML automatic verification tool with formal methods. In: Minas, M. (ed.) Proceedings of the Workshop on Visual Languages and Formal Methods, VLFM 2004, Rome, Italy, September 30, 2004, Series. Electronic Notes in Theoretical Computer Science, vol. 127, pp. 3\u201316. Elsevier (2004)","DOI":"10.1016\/j.entcs.2004.10.024"},{"key":"1281_CR61","doi-asserted-by":"crossref","unstructured":"Lam, V.S.W., Padget, J.A.: Symbolic model checking of UML statechart diagrams with an integrated approach. In: 11th IEEE International Conference on the Engineering of Computer-Based Systems (ECBS 2004), 24-27 May 2004, Brno, Czech Republic. IEEE Computer Society, pp. 337\u2013347 (2004)","DOI":"10.1109\/ECBS.2004.1316717"},{"key":"1281_CR62","doi-asserted-by":"crossref","unstructured":"Schneider, F., Easterbrook, S.M., Callahan, J.R., Holzmann, G.J.: Validating requirements for fault tolerant systems using model checking. In: 3rd International Conference on Requirements Engineering (ICRE \u201998), Putting Requirements Engineering to Practice, April 6-10, 1998, Colorado Springs, CO, USA, Proceedings. IEEE Computer Society, pp. 4\u201313 (1998)","DOI":"10.1109\/ICRE.1998.667803"},{"key":"1281_CR63","doi-asserted-by":"crossref","unstructured":"Gluck, P., Holzmann, G.: Using SPIN model checking for flight software verification. In: Proceedings, IEEE Aerospace Conference, vol.\u00a01, p. 1 (2002)","DOI":"10.1109\/AERO.2002.1036832"},{"issue":"8","key":"1281_CR64","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M.R., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749\u2013765 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"1281_CR65","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"issue":"12","key":"1281_CR66","first-page":"695","volume":"17","author":"R Krishnan","year":"2020","unstructured":"Krishnan, R., Lalithambika, V.R.: Modeling and validating launch vehicle onboard software using the SPIN model checker. J. Aerosp. Inf. Syst. 17(12), 695\u2013699 (2020)","journal-title":"J. Aerosp. Inf. Syst."},{"key":"1281_CR67","unstructured":"Brat, G., Denney, E., Giannakopoulou, D., Frank, Jonsson, A.: Verification of autonomous systems for space applications. In: 2006 IEEE Aerospace Conference, pp. 11 (2006)"},{"key":"1281_CR68","volume-title":"State Models and Java Programs","author":"J Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: State Models and Java Programs. Wiley, Hoboken (1999)"},{"key":"1281_CR69","doi-asserted-by":"crossref","unstructured":"Esteve, M., Katoen, J., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland, IEEE Computer Society, pp. 1022\u20131031 (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"1281_CR70","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Cimatti, A., Katoen, J., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) Computer Safety, Reliability, and Security, 28th International Conference, SAFECOMP 2009, Hamburg, Germany, September 15-18, 2009. Proceedings, Series. Lecture Notes in Computer Science, vol. 5775, pp. 173\u2013186. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04468-7_15"},{"key":"1281_CR71","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jss.2018.07.053","volume":"145","author":"E Stachtiari","year":"2018","unstructured":"Stachtiari, E., Mavridou, A., Katsaros, P., Bliudze, S., Sifakis, J.: Early validation of system requirements and design through correctness-by-construction. J. Syst. Softw. 145, 52\u201378 (2018)","journal-title":"J. Syst. Softw."},{"key":"1281_CR72","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Series. Lecture Notes in Computer Science, vol. 8559, pp. 334\u2013342. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"1281_CR73","doi-asserted-by":"crossref","unstructured":"Nardone, V., Santone, A., Tipaldi, M., Glielmo, L.: Probabilistic model checking applied to autonomous spacecraft reconfiguration. In: IEEE Metrology for Aerospace (MetroAeroSpace), pp. 556\u2013560 (2016)","DOI":"10.1109\/MetroAeroSpace.2016.7573276"},{"key":"1281_CR74","doi-asserted-by":"crossref","unstructured":"Peng, Z., Lu, Y., Miller, A., Johnson, C.W., Zhao, T.: A probabilistic model checking approach to analysing reliability, availability, and maintainability of a single satellite system. In: Al-Dabass, D., Orsoni, A., Xie, Z. (eds.) Seventh UKSim, AMSS European Modelling Symposium, EMS,: 20\u201322 November, 2013, Manchester UK, pp. 611\u2013616. IEEE (2013)","DOI":"10.1109\/EMS.2013.102"},{"key":"1281_CR75","doi-asserted-by":"crossref","unstructured":"Andersen, J.R., Andersen, N., Enevoldsen, S., Hansen, M.M., Larsen, K.G., Olesen, S.R., Srba, J., Wortmann, J.K.: CAAL: concurrency workbench, Aalborg edition. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) Theoretical Aspects of Computing\u2014ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, Series. Lecture Notes in Computer Science, vol. 9399, pp. 573\u2013582. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-25150-9_33"},{"key":"1281_CR76","doi-asserted-by":"crossref","unstructured":"Chan N., Mitra, S.: Verifying safety of an autonomous spacecraft rendezvous mission. In: Frehse, G., Althoff, M. (eds.) ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, Collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA, Series. EPiC Series in Computing, vol.\u00a048, pp. 20\u201332. EasyChair (2017)","DOI":"10.29007\/thb4"},{"key":"1281_CR77","unstructured":"Jacklin, S.A.: Survey of verification and validation techniques for small satellite software development. Tech. Rep. (2015)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01281-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-025-01281-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01281-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T02:20:10Z","timestamp":1763173210000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-025-01281-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,15]]},"references-count":77,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["1281"],"URL":"https:\/\/doi.org\/10.1007\/s10270-025-01281-6","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,15]]},"assertion":[{"value":"14 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 January 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 March 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 April 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}