{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T13:14:46Z","timestamp":1780492486120,"version":"3.54.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,5,11]],"date-time":"2025-05-11T00:00:00Z","timestamp":1746921600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,11]],"date-time":"2025-05-11T00:00:00Z","timestamp":1746921600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000133658\/21\/NL\/CRS"],"award-info":[{"award-number":["4000133658\/21\/NL\/CRS"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000133658\/21\/NL\/CRS"],"award-info":[{"award-number":["4000133658\/21\/NL\/CRS"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000133658\/21\/NL\/CRS"],"award-info":[{"award-number":["4000133658\/21\/NL\/CRS"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000133658\/21\/NL\/CRS"],"award-info":[{"award-number":["4000133658\/21\/NL\/CRS"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000133658\/21\/NL\/CRS"],"award-info":[{"award-number":["4000133658\/21\/NL\/CRS"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000844","name":"European Space Agency","doi-asserted-by":"publisher","award":["4000133658\/21\/NL\/CRS"],"award-info":[{"award-number":["4000133658\/21\/NL\/CRS"]}],"id":[{"id":"10.13039\/501100000844","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,9]]},"DOI":"10.1007\/s11334-025-00607-3","type":"journal-article","created":{"date-parts":[[2025,5,10]],"date-time":"2025-05-10T22:27:51Z","timestamp":1746916071000},"page":"961-984","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Specification and model-checking of space systems in the TASTE toolset"],"prefix":"10.1007","volume":"21","author":[{"given":"Iulia","family":"Dragomir","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlos","family":"Redondo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tiago","family":"Jorge","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laura","family":"Gouveia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Iulian","family":"Ober","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maxime","family":"Perrotin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,11]]},"reference":[{"key":"607_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Symposium on programming","author":"J Queille","year":"1982","unstructured":"Queille J, Sifakis J, Dezani-Ciancaglini M, Montanari U (1982) Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini M, Montanari U (eds) Symposium on programming, vol 137. Lecture notes in computer science. Springer, pp 337\u2013351"},{"issue":"2","key":"607_CR2","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263","journal-title":"ACM Trans Program Lang Syst"},{"key":"607_CR3","unstructured":"TASTE (2023) The assert set of tools for engineering. Available at https:\/\/www.taste.tools\/"},{"key":"607_CR4","unstructured":"Dragomir I et al (2021) Formal verification of space systems designed with TASTE. In: ESA (ed) Proceedings of 2nd workshop on model based space systems and software engineering (MBSE 2021)"},{"key":"607_CR5","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-540-30080-9_8","volume-title":"SFM","author":"M Bozga","year":"2004","unstructured":"Bozga M, Graf S, Ober I, Ober I, Sifakis J, Bernardo M, Corradini F (2004) The IF toolset. In: Bernardo M, Corradini F (eds) SFM, vol 3185. Lecture notes in computer science. Springer, pp 237\u2013267"},{"key":"607_CR6","volume-title":"The SPIN model checker: primer and reference manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann G (2011) The SPIN model checker: primer and reference manual, 1st edn. Addison-Wesley Professional","edition":"1"},{"key":"607_CR7","unstructured":"ITU-T (2021) Abstract syntax notation one (ASN.1): Specification of basic notation"},{"key":"607_CR8","unstructured":"SAE (2022) Architecture analysis and design language (AADL). Available at https:\/\/www.sae.org\/standards\/content\/as5506d\/"},{"key":"607_CR9","unstructured":"ITU-T (2010) Specification and description language (SDL). Available at https:\/\/www.itu.int\/rec\/T-REC-Z.100\/en"},{"key":"607_CR10","unstructured":"LOTOS (1989). Available at https:\/\/www.iso.org\/standard\/16258.html"},{"key":"607_CR11","unstructured":"SPIN (2020). Available at http:\/\/spinroot.com\/spin\/whatispin.html"},{"key":"607_CR12","unstructured":"UPPAAL (2019). Available at http:\/\/www.uppaal.org"},{"key":"607_CR13","unstructured":"Java PathFinder (2020). Available at https:\/\/software.nasa.gov\/software\/ARC-17487-1"},{"key":"607_CR14","unstructured":"LTSmin (2020). Available at https:\/\/ltsmin.utwente.nl"},{"key":"607_CR15","unstructured":"PRISM model checker (2020). Available at https:\/\/www.prismmodelchecker.org"},{"key":"607_CR16","unstructured":"Ocon J et al (2019) Testing autonomous robots: a discussion on performances obtained during the ERGO field tests. In: ESA (ed) Proceedings of 15th symposium on advanced space technologies in robotics and automation"},{"key":"607_CR17","unstructured":"MoC4Space (2023) TASTE model-checking with IF\u2014git repository. Available at https:\/\/gitrepos.estec.esa.int\/taste\/if-model-checking"},{"key":"607_CR18","unstructured":"Dragomir I et al (2022) Model-checking for TASTE designed space software systems: results and lessons learned. In: ESA (ed) Proceedings of 3rd workshop on model based space systems and software engineering (MBSE 2022)"},{"key":"607_CR19","unstructured":"PragmaDev (2023) Pragmadev Studio. Available at https:\/\/www.pragmadev.com\/product\/studio.html"},{"issue":"2","key":"607_CR20","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/spe.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann G, David A, Larsen KG, Pettersson P, Yi W (2011) Developing UPPAAL over 15 years. Softw Pract Exp 41(2):133\u2013142","journal-title":"Softw Pract Exp"},{"key":"607_CR21","unstructured":"Holzmann GJ (2004) The SPIN model checker\u2014primer and reference manual. Addison-Wesley"},{"key":"607_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"CAV","author":"A Cimatti","year":"2002","unstructured":"Cimatti A et al (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) CAV, vol 2404. Lecture notes in computer science. Springer, pp 359\u2013364"},{"key":"607_CR23","doi-asserted-by":"crossref","unstructured":"Barnett M, Chang BE, DeLine R, Jacobs B, Leino KRM, de Boer FS, Bonsangue MM, Graf S, de Roever WP (2005) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS, Bonsangue MM, Graf S, de Roever WP (eds) FMCO, vol 4111. Lecture notes in computer science. Springer, pp 364\u2013387","DOI":"10.1007\/11804192_17"},{"key":"607_CR24","doi-asserted-by":"crossref","unstructured":"Bozzano M et al (2019) COMPASS 3.0. In: Vojnar T, Zhang L (eds) TACAS (1), vol 11427. Lecture notes in computer science. Springer, pp 379\u2013385","DOI":"10.1007\/978-3-030-17462-0_25"},{"key":"607_CR25","unstructured":"Kurowski M, Babski R, Duncan S, Perrotin M, Webster M (2021) Model-checking for formal verification of space systems. In: ESA (ed) Proceedings of 2nd workshop on model based space systems and software engineering (MBSE 2021)"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-025-00607-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-025-00607-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-025-00607-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,6]],"date-time":"2025-09-06T14:28:24Z","timestamp":1757168904000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-025-00607-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,11]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["607"],"URL":"https:\/\/doi.org\/10.1007\/s11334-025-00607-3","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,11]]},"assertion":[{"value":"13 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}