{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T15:08:00Z","timestamp":1774883280496,"version":"3.50.1"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:00:00Z","timestamp":1767916800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:00:00Z","timestamp":1767916800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2026,5]]},"DOI":"10.1007\/s10664-025-10786-z","type":"journal-article","created":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:31:48Z","timestamp":1767925908000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Aiding the design of critical software systems by iterative exploration of distinct requirement violation scenarios"],"prefix":"10.1007","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1307-3332","authenticated-orcid":false,"given":"Rich\u00e1rd","family":"Szab\u00f3","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2912-028X","authenticated-orcid":false,"given":"D\u00e1niel","family":"Szekeres","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon J\u00f3zsef","family":"Nagy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zolt\u00e1n","family":"Thim\u00e1r","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1184-2882","authenticated-orcid":false,"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1846-261X","authenticated-orcid":false,"given":"Zolt\u00e1n","family":"Micskei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-3563","authenticated-orcid":false,"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,9]]},"reference":[{"key":"10786_CR1","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press"},{"key":"10786_CR2","doi-asserted-by":"publisher","unstructured":"Bengtsson J, Larsen K, Larsson F et al (1995) UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: International hybrid systems workshop, Springer, pp 232\u2013243, https:\/\/doi.org\/10.1007\/BFb0020949","DOI":"10.1007\/BFb0020949"},{"issue":"3","key":"10786_CR3","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/S0951-8320(00)00078-8","volume":"71","author":"C Bernardeschi","year":"2001","unstructured":"Bernardeschi C, Fantechi A, Gnesi S (2001) Formal validation of fault-tolerance mechanisms inside GUARDS. Reliab Eng Syst Saf 71(3):261\u2013270. https:\/\/doi.org\/10.1016\/S0951-8320(00)00078-8","journal-title":"Reliab Eng Syst Saf"},{"issue":"4","key":"10786_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1002\/stvr.258","volume":"12","author":"C Bernardeschi","year":"2002","unstructured":"Bernardeschi C, Fantechi A, Gnesi S (2002) Model checking fault tolerant systems. Softw Test Verification Reliab 12(4):251\u2013275. https:\/\/doi.org\/10.1002\/stvr.258","journal-title":"Softw Test Verification Reliab"},{"key":"10786_CR5","doi-asserted-by":"publisher","unstructured":"Bittner B, Bozzano M, Cavada R et al (2016a) The xSAP safety analysis platform. In: Chechik M, Raskin J (eds) TACAS \u201916, LNCS, vol 9636. Springer, pp 533\u2013539, https:\/\/doi.org\/10.1007\/978-3-662-49674-9_31","DOI":"10.1007\/978-3-662-49674-9_31"},{"key":"10786_CR6","unstructured":"Bittner B, Bozzano M, Cimatti A et al (2016b) Automated synthesis of timed failure propagation graphs. In: IJCAI, pp 972\u2013978"},{"key":"10786_CR7","doi-asserted-by":"publisher","unstructured":"Bozzano M, Cimatti A, Fernandes\u00a0Pires A et al (2015a) Formal design and safety analysis of AIR6110 wheel brake system. In: CAV \u201915, Springer, pp 518\u2013535, https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36","DOI":"10.1007\/978-3-319-21690-4_36"},{"key":"10786_CR8","doi-asserted-by":"publisher","unstructured":"Bozzano M, Cimatti A, Griggio A et al (2015b) Efficient anytime techniques for model-based safety analysis. In: CAV \u201915, LNCS, vol 9206. Springer, pp 603\u2013621, https:\/\/doi.org\/10.1007\/978-3-319-21690-4_41","DOI":"10.1007\/978-3-319-21690-4_41"},{"key":"10786_CR9","doi-asserted-by":"publisher","unstructured":"Bozzano M, Munk P, Schweizer M et al (2020) Model-based safety analysis of mode transitions. In: SAFECOMP \u201920, Springer, pp 99\u2013114, https:\/\/doi.org\/10.1007\/978-3-030-54549-9_7","DOI":"10.1007\/978-3-030-54549-9_7"},{"key":"10786_CR10","doi-asserted-by":"publisher","unstructured":"Cavada R, Cimatti A, Dorigatti M et al (2014) The nuXmv symbolic model checker. In: CAV \u201914, LNCS, vol 8559. Springer, pp 334\u2013342, https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"1","key":"10786_CR11","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/S0951-8320(03)00059-0","volume":"82","author":"SD Cha","year":"2003","unstructured":"Cha SD, Son HS, Yoo J et al (2003) Systematic evaluation of fault trees using real-time model checker UPPAAL. Reliab Eng Syst Saf 82(1):11\u201320. https:\/\/doi.org\/10.1016\/S0951-8320(03)00059-0","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR12","doi-asserted-by":"publisher","unstructured":"Cimatti A, Clarke E, Giunchiglia E et al (2002) NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: CAV \u201902, LNCS, vol 2404. Springer, Copenhagen, Denmark, https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"10786_CR13","doi-asserted-by":"publisher","unstructured":"Cimatti A, Griggio A, Mover S et al (2014) IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m E, Havelund K (eds) Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, Lecture Notes in Computer Science, vol 8413. Springer, pp 46\u201361, https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"10786_CR14","doi-asserted-by":"publisher","unstructured":"Clarke EM, Grumberg O, Jha S et al (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, Lecture Notes in Computer Science, vol 1855. Springer, pp 154\u2013169, https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"10786_CR15","doi-asserted-by":"publisher","unstructured":"Elmqvist J, Nadjm-Tehrani S (2008) Tool support for incremental failure mode and effects analysis of component-based systems. In: DATE \u201908. ACM, pp 921\u2013927, https:\/\/doi.org\/10.1109\/DATE.2008.4484792","DOI":"10.1109\/DATE.2008.4484792"},{"issue":"1","key":"10786_CR16","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson EA, Halpern JY (1986) \u201cSometimes\u2019\u2019 and \u201cnot never\u2019\u2019 revisited: On branching versus linear time temporal logic. Journal of the ACM (JACM) 33(1):151\u2013178. https:\/\/doi.org\/10.1145\/4904.4999","journal-title":"Journal of the ACM (JACM)"},{"issue":"9","key":"10786_CR17","doi-asserted-by":"publisher","first-page":"3664","DOI":"10.1109\/TSE.2021.3101818","volume":"48","author":"K Gaaloul","year":"2022","unstructured":"Gaaloul K, Menghi C, Nejati S et al (2022) Combining genetic programming and model checking to generate environment assumptions. IEEE Trans Software Eng 48(9):3664\u20133685. https:\/\/doi.org\/10.1109\/TSE.2021.3101818","journal-title":"IEEE Trans Software Eng"},{"key":"10786_CR18","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.ress.2019.02.005","volume":"186","author":"M Ghadhab","year":"2019","unstructured":"Ghadhab M, Junges S, Katoen J et al (2019) Safety analysis for vehicle guidance systems with dynamic fault trees. Reliab Eng Syst Saf 186:37\u201350. https:\/\/doi.org\/10.1016\/j.ress.2019.02.005","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR19","doi-asserted-by":"publisher","unstructured":"Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 23-27 September 2002, Edinburgh, Scotland, UK. IEEE Computer Society, pp 3\u201312, https:\/\/doi.org\/10.1109\/ASE.2002.1114984","DOI":"10.1109\/ASE.2002.1114984"},{"issue":"6","key":"10786_CR20","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 (2020) Formal methods in dependable systems engineering: A survey of professionals from europe and north america. Empir Softw Eng 25(6):4473\u20134546. https:\/\/doi.org\/10.1007\/S10664-020-09836-5","journal-title":"Empir Softw Eng"},{"key":"10786_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2020.106923","volume":"199","author":"D Gouyon","year":"2020","unstructured":"Gouyon D, P\u00e9tin J, Cochard T et al (2020) Architecture assessment for safety critical plant operation using reachability analysis of timed automata. Reliab Eng Syst Saf 199:106923. https:\/\/doi.org\/10.1016\/j.ress.2020.106923","journal-title":"Reliab Eng Syst Saf"},{"issue":"6","key":"10786_CR22","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 et al (2020) Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw Syst Model 19(6):1483\u20131517. https:\/\/doi.org\/10.1007\/s10270-020-00806-5","journal-title":"Softw Syst Model"},{"key":"10786_CR23","doi-asserted-by":"publisher","unstructured":"Graics B, Mondok M, Moln\u00e1r V et al (2025) Model-based testing of asynchronously communicating distributed controllers using validated mappings to formal representations. Science of Computer Programming p 103265. https:\/\/doi.org\/10.1016\/j.scico.2025.103265","DOI":"10.1016\/j.scico.2025.103265"},{"key":"10786_CR24","doi-asserted-by":"publisher","unstructured":"Harel D, Thiagarajan P (2003) Message sequence charts. UML for real: design of embedded real-time systems pp 77\u2013105. https:\/\/doi.org\/10.1007\/0-306-48738-1_4","DOI":"10.1007\/0-306-48738-1_4"},{"key":"10786_CR25","doi-asserted-by":"publisher","unstructured":"Heizmann M, Hoenicke J, Podelski A (2013) Software model checking for people who love automata. In: Sharygina N, Veith H (eds) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, vol 8044. Springer, pp 36\u201352, https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"10786_CR26","doi-asserted-by":"publisher","unstructured":"Henzinger TA, Jhala R, Majumdar R et al (2002) Lazy abstraction. In: Launchbury J, Mitchell JC (eds) Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002. ACM, pp 58\u201370, https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"issue":"5","key":"10786_CR27","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Software Eng 23(5):279\u2013295. https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans Software Eng"},{"key":"10786_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2020.106822","volume":"198","author":"C Huang","year":"2020","unstructured":"Huang C, Li L (2020) Architectural design and analysis of a steer-by-wire system in view of functional safety concept. Reliab Eng Syst Saf 198:106822. https:\/\/doi.org\/10.1016\/j.ress.2020.106822","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR29","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.arcontrol.2019.04.001","volume":"47","author":"C Huang","year":"2019","unstructured":"Huang C, Naghdy F, Du H et al (2019) Fault tolerant steer-by-wire systems: An overview. Annu Rev Control 47:98\u2013111. https:\/\/doi.org\/10.1016\/j.arcontrol.2019.04.001","journal-title":"Annu Rev Control"},{"key":"10786_CR30","unstructured":"ISO (2011) Road vehicles\u2014functional safety. ISO 26262:2011, International Organization for Standardization, Geneva, Switzerland"},{"key":"10786_CR31","doi-asserted-by":"publisher","unstructured":"Jhala R, Majumdar R (2009) Software model checking. ACM Comput Surv 41(4):21:1\u201321:54. https:\/\/doi.org\/10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"issue":"4","key":"10786_CR32","doi-asserted-by":"publisher","first-page":"3317","DOI":"10.1109\/TDSC.2022.3203805","volume":"20","author":"LA Jimenez-Roa","year":"2023","unstructured":"Jimenez-Roa LA, Heskes T, Tinga T et al (2023) Automatic inference of fault tree models via multi-objective evolutionary algorithms. IEEE Trans Dependable Secur Comput 20(4):3317\u20133327. https:\/\/doi.org\/10.1109\/TDSC.2022.3203805","journal-title":"IEEE Trans Dependable Secur Comput"},{"issue":"5","key":"10786_CR33","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/S10664-023-10353-4","volume":"28","author":"AP Kaleeswaran","year":"2023","unstructured":"Kaleeswaran AP, Nordmann A, Vogel T et al (2023) A user study for evaluation of formal verification results and their explanation at Bosch. Empir Softw Eng 28(5):125. https:\/\/doi.org\/10.1007\/S10664-023-10353-4","journal-title":"Empir Softw Eng"},{"key":"10786_CR34","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.ress.2013.06.007","volume":"120","author":"E Kang","year":"2013","unstructured":"Kang E, Enoiu EP, Marinescu R et al (2013) A methodology for formal analysis and verification of EAST-ADL models. Reliab Eng Syst Saf 120:127\u2013138. https:\/\/doi.org\/10.1016\/j.ress.2013.06.007","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR35","doi-asserted-by":"publisher","unstructured":"K\u00f6lbl M, Leue S (2018) Automated functional safety analysis of automated driving systems. In: Howar F, Barnat J (eds) FMICS \u201918, LNCS, vol 11119. Springer, pp 35\u201351, https:\/\/doi.org\/10.1007\/978-3-030-00244-2_3","DOI":"10.1007\/978-3-030-00244-2_3"},{"key":"10786_CR36","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.ress.2012.03.021","volume":"105","author":"J Lahtinen","year":"2012","unstructured":"Lahtinen J, Valkonen J, Bj\u00f6rkman K et al (2012) Model checking of safety-critical software in the nuclear engineering domain. Reliab Eng Syst Saf 105:104\u2013113. https:\/\/doi.org\/10.1016\/j.ress.2012.03.021","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR37","doi-asserted-by":"publisher","unstructured":"Lee EA, Sangiovanni-Vincentelli AL (2011) Component-based design for the future. In: 2011 Design, Automation & Test in Europe, IEEE, pp 1\u20135, https:\/\/doi.org\/10.1109\/DATE.2011.5763168","DOI":"10.1109\/DATE.2011.5763168"},{"key":"10786_CR38","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/j.ress.2013.06.045","volume":"120","author":"R Mader","year":"2013","unstructured":"Mader R, Armengaud E, Grie\u00dfnig G et al (2013) OASIS: an automotive analysis and safety engineering instrument. Reliab Eng Syst Saf 120:150\u2013162. https:\/\/doi.org\/10.1016\/j.ress.2013.06.045","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR39","doi-asserted-by":"publisher","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: CAV\u201906, https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"10786_CR40","doi-asserted-by":"publisher","unstructured":"Miller S, Anderson E, Wagner L et al (2005) Formal verification of flight critical software. In: AIAA Guidance, Navigation, and Control Conference and Exhibit, p 6431, https:\/\/doi.org\/10.2514\/6.2005-6431","DOI":"10.2514\/6.2005-6431"},{"key":"10786_CR41","doi-asserted-by":"publisher","unstructured":"Moln\u00e1r V, Graics B, V\u00f6r\u00f6s A et al (2018) The Gamma Statechart Composition Framework: design, verification and code generation for component-based reactive systems. In: ICSE \u201918. ACM, pp 113\u2013116, https:\/\/doi.org\/10.1145\/3183440.3183489","DOI":"10.1145\/3183440.3183489"},{"issue":"4","key":"10786_CR42","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1109\/TDSC.2018.2846741","volume":"17","author":"A Munir","year":"2020","unstructured":"Munir A, Koushanfar F (2020) Design and analysis of secure and dependable automotive CPS: A steer-by-wire case study. IEEE Trans Dependable Secur Comput 17(4):813\u2013827. https:\/\/doi.org\/10.1109\/TDSC.2018.2846741","journal-title":"IEEE Trans Dependable Secur Comput"},{"issue":"2","key":"10786_CR43","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1109\/TDSC.2014.2320714","volume":"12","author":"S Ni","year":"2015","unstructured":"Ni S, Zhuang Y, Cao Z et al (2015) Modeling dependability features for real-time embedded systems. IEEE Trans Dependable Secur Comput 12(2):190\u2013203. https:\/\/doi.org\/10.1109\/TDSC.2014.2320714","journal-title":"IEEE Trans Dependable Secur Comput"},{"issue":"3","key":"10786_CR44","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0951-8320(03)00090-5","volume":"81","author":"F Ortmeier","year":"2003","unstructured":"Ortmeier F, Schellhorn G, Thums A et al (2003) Safety analysis of the height control system for the elbtunnel. Reliab Eng Syst Saf 81(3):259\u2013268. https:\/\/doi.org\/10.1016\/S0951-8320(03)00090-5","journal-title":"Reliab Eng Syst Saf"},{"issue":"4","key":"10786_CR45","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1007\/S10664-013-9251-2","volume":"19","author":"A Osaiweran","year":"2014","unstructured":"Osaiweran A, Schuts M, Hooman J (2014) Experiences with incorporating formal techniques into industrial practice. Empir Softw Eng 19(4):1169\u20131194. https:\/\/doi.org\/10.1007\/S10664-013-9251-2","journal-title":"Empir Softw Eng"},{"key":"10786_CR46","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2020.107237","volume":"205","author":"A Pakonen","year":"2021","unstructured":"Pakonen A, Buzhinsky I, Bj\u00f6rkman K (2021) Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems. Reliab Eng Syst Saf 205:107237. https:\/\/doi.org\/10.1016\/j.ress.2020.107237","journal-title":"Reliab Eng Syst Saf"},{"issue":"1","key":"10786_CR47","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/S10664-012-9215-Y","volume":"19","author":"RP Pontes","year":"2014","unstructured":"Pontes RP, V\u00e9ras PC, Ambrosio AM et al (2014) Contributions of model checking and cofi methodology to the development of space embedded software. Empir Softw Eng 19(1):39\u201368. https:\/\/doi.org\/10.1007\/S10664-012-9215-Y","journal-title":"Empir Softw Eng"},{"issue":"1","key":"10786_CR48","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1109\/TDSC.2018.2883057","volume":"18","author":"B Poudel","year":"2021","unstructured":"Poudel B, Munir A (2021) Design and evaluation of a reconfigurable ECU architecture for secure and dependable automotive cps. IEEE Trans Dependable Secur Comput 18(1):235\u2013252. https:\/\/doi.org\/10.1109\/TDSC.2018.2883057","journal-title":"IEEE Trans Dependable Secur Comput"},{"key":"10786_CR49","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.scico.2013.10.005","volume":"90","author":"V Rupanov","year":"2014","unstructured":"Rupanov V, Buckl C, Fiege L et al (2014) Employing early model-based safety evaluation to iteratively derive E\/E architecture design. Sci Comput Program 90:161\u2013179. https:\/\/doi.org\/10.1016\/j.scico.2013.10.005","journal-title":"Sci Comput Program"},{"issue":"2","key":"10786_CR50","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0951-8320(01)00092-8","volume":"75","author":"J Rushby","year":"2002","unstructured":"Rushby J (2002) Using model checking to help discover mode confusions and other automation surprises. Reliab Eng Syst Saf 75(2):167\u2013177. https:\/\/doi.org\/10.1016\/S0951-8320(01)00092-8","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR51","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/j.ress.2014.10.025","volume":"135","author":"S Sharvia","year":"2015","unstructured":"Sharvia S, Papadopoulos Y (2015) Integrating model checking with hip-hops in model-based safety analysis. Reliab Eng Syst Saf 135:64\u201380. https:\/\/doi.org\/10.1016\/j.ress.2014.10.025","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR52","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2021.107649","volume":"213","author":"D Stewart","year":"2021","unstructured":"Stewart D, Liu J, Cofer DD et al (2021) AADL-based safety analysis using formal methods applied to aircraft digital systems. Reliab Eng Syst Saf 213:107649. https:\/\/doi.org\/10.1016\/j.ress.2021.107649","journal-title":"Reliab Eng Syst Saf"},{"key":"10786_CR53","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10256749","author":"R Szab\u00f3","year":"2023","unstructured":"Szab\u00f3 R, Szekeres D, Nagy SJ et al (2023) Supplementary material for \u201caiding the design of critical software systems by iterative exploration of distinct requirement violation scenarios\u2019\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.10256749","journal-title":"Zenodo"},{"key":"10786_CR54","doi-asserted-by":"publisher","unstructured":"Tonetta S (2009) Abstract model checking without computing the abstraction. In: Cavalcanti A, Dams D (eds) FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, Lecture Notes in Computer Science, vol 5850. Springer, pp 89\u2013105, https:\/\/doi.org\/10.1007\/978-3-642-05089-3_7","DOI":"10.1007\/978-3-642-05089-3_7"},{"key":"10786_CR55","doi-asserted-by":"publisher","unstructured":"T\u00f3th T, Hajdu A, V\u00f6r\u00f6s A et al (2017) Theta: a framework for abstraction refinement-based model checking. In: FMCAD 2017, pp 176\u2013179, https:\/\/doi.org\/10.23919\/FMCAD.2017.8102257","DOI":"10.23919\/FMCAD.2017.8102257"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-025-10786-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10664-025-10786-z","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-025-10786-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T14:36:12Z","timestamp":1774881372000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10664-025-10786-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,9]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,5]]}},"alternative-id":["10786"],"URL":"https:\/\/doi.org\/10.1007\/s10664-025-10786-z","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,9]]},"assertion":[{"value":"1 March 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 November 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 January 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"BME has a research and consultation contract with thyssenkrupp Components Technology Hungary Ltd.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of Interest"}}],"article-number":"58"}}