{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T00:27:35Z","timestamp":1770683255441,"version":"3.49.0"},"reference-count":152,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T00:00:00Z","timestamp":1740700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T00:00:00Z","timestamp":1740700800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"ISTI - PISA"}],"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>Formal methods and tools are successfully applied to the development of safety-critical systems for decades now, in particular in the transport domain, without a single technique or tool emerging as the dominant solution for system design. Formal methods are highly recommended by the existing safety standards in the railway industry, but railway engineers typically lack the knowledge to transform their semi-formal models into a formal model, with a precise semantics, that can serve as input to formal methods tools. We share the results of performing empirical studies in the field, including usability analyses of formal methods tools involving railway practitioners. We discuss, in particular with respect to railway systems and their modelling, our experiences in applying formal methods and tools to a variety of case studies, for which we interacted with a number of companies from the railway domain. We report on lessons learned from these experiences and provide pointers to steer future research towards facilitating further synergies between researchers and developers of formal methods and tools on the one hand and practitioners from the railway industry on the other.<\/jats:p>","DOI":"10.1007\/s10270-025-01276-3","type":"journal-article","created":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T00:10:16Z","timestamp":1740701416000},"page":"1935-1954","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Models for formal methods and tools: the case of railway systems"],"prefix":"10.1007","volume":"24","author":[{"given":"M. H.","family":"ter Beek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,2,28]]},"reference":[{"key":"1276_CR1","doi-asserted-by":"publisher","DOI":"10.1002\/9781119005056","volume-title":"CENELEC 50128 and IEC 62279 standards","author":"J-L Boulanger","year":"2015","unstructured":"Boulanger, J.-L.: CENELEC 50128 and IEC 62279 standards. Wiley, Hoboken (2015). https:\/\/doi.org\/10.1002\/9781119005056"},{"key":"1276_CR2","unstructured":"European Committee for Electrotechnical Standardization: CENELEC EN 50128\u00a0\u2014 Railway applications\u2013communication, signalling and processing systems\u2013software for railway control and protection systems. https:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128 (2011)"},{"key":"1276_CR3","doi-asserted-by":"publisher","unstructured":"Guiho, G., Hennebert, C.: SACEM Software Validation. In: Proceedings of the 12th International Conference on Software Engineering (ICSE\u201990), pp. 186\u2013191. IEEE, (1990). https:\/\/doi.org\/10.1109\/ICSE.1990.63621","DOI":"10.1109\/ICSE.1990.63621"},{"key":"1276_CR4","unstructured":"DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: Subway speed control system. In: Diaz, M., Groz, R. (eds.) Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992). IFIP Transactions, vol. C-10, pp. 199\u2013213. North-Holland, The Netherlands (1992)"},{"issue":"1","key":"1276_CR5","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/tsi.22.11-32","volume":"22","author":"D Doll\u00e9","year":"2003","unstructured":"Doll\u00e9, D., Essam\u00e9, D., Falampin, J.: B dans le transport ferroviaire: L\u2019exp\u00e9rience de Siemens transportation systems. Tech. Sci. Inf. 22(1), 11\u201332 (2003). https:\/\/doi.org\/10.3166\/tsi.22.11-32","journal-title":"Tech. Sci. Inf."},{"key":"1276_CR6","doi-asserted-by":"publisher","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in Large Scale Projects: The Canarsie Line CBTC Experience. In: Julliand, J., Kouchnarenko, O. (eds.) Proceedings of the 7th International Conference of B Users (B\u201907). LNCS, vol. 4355, pp. 252\u2013254. Springer, (2007). https:\/\/doi.org\/10.1007\/11955757_21","DOI":"10.1007\/11955757_21"},{"key":"1276_CR7","doi-asserted-by":"publisher","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: A successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) Proceedings of the 1st World Congress on Formal Methods in the Development of Computing Systems (FM\u201999). LNCS, vol. 1708, pp. 369\u2013387. Springer, (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_22","DOI":"10.1007\/3-540-48119-2_22"},{"key":"1276_CR8","doi-asserted-by":"publisher","unstructured":"Comptier, M., Leuschel, M., Mejia, L.-F., Molinero Perez, J., Mutz, M.: Property-based modelling and validation of a CBTC zone controller in event-B. In: Collart Dutilleul, S., Lecomte, T., Romanovsky, A.B. (eds.) Proceedings of the 3rd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201919). LNCS, vol. 11495, pp. 202\u2013212. Springer, (2019).https:\/\/doi.org\/10.1007\/978-3-030-18744-6_13","DOI":"10.1007\/978-3-030-18744-6_13"},{"issue":"7","key":"1276_CR9","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1016\/j.scico.2012.04.003","volume":"78","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Grasso, D., Magnani, G., Fantechi, A., Tempestini, M.: The Metr\u00f4 Rio case study. Sci. Comput. Program. 78(7), 828\u2013842 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.04.003","journal-title":"Sci. Comput. Program."},{"key":"1276_CR10","doi-asserted-by":"publisher","unstructured":"Chiappini, A., Cimatti, A., Macchi, L., Rebollo, O., Roveri, M., Susi, A., Tonetta, S., Vittorini, B.: Formalization and validation of a subset of the European Train Control System. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering (ICSE\u201910), vol. 2, pp. 109\u2013118. ACM, (2010). https:\/\/doi.org\/10.1145\/1810295.1810312","DOI":"10.1145\/1810295.1810312"},{"issue":"3","key":"1276_CR11","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-020-00562-3","volume":"22","author":"M Butler","year":"2020","unstructured":"Butler, M., Hoang, T.S., Raschke, A., Reichl, K.: Introduction to the special section on the ABZ 2018 case study: hybrid ERTMS\/ETCS level 3. Int. J. Softw. Tools Technol. Transf. 22(3), 249\u2013255 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00562-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1276_CR12","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10009-019-00525-3","volume":"22","author":"J-R Abrial","year":"2020","unstructured":"Abrial, J.-R.: The ABZ-2018 case study with Event-B. Int. J. Softw. Tools Technol. Transf. 22(3), 257\u2013264 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00525-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR13","doi-asserted-by":"publisher","unstructured":"Arcaini, P., Kofro\u0148, J., Je\u017eek, P.: Validation of the hybrid ERTMS\/ETCS level 3 using spin. Int. J. Softw. Tools Technol. Transf. 22(3), 265\u2013279 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00539-x","DOI":"10.1007\/s10009-019-00539-x"},{"issue":"3","key":"1276_CR14","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10009-019-00540-4","volume":"22","author":"A Cunha","year":"2020","unstructured":"Cunha, A., Macedo, N.: Validating the hybrid ERTMS\/ETCS level 3 concept with Electrum. Int. J. Softw. Tools Technol. Transf. 22(3), 281\u2013296 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00540-4","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1276_CR15","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10009-019-00548-w","volume":"22","author":"D Dghaym","year":"2020","unstructured":"Dghaym, D., Dalvandi, M., Poppleton, M., Snook, C.: Formalising the hybrid ERTMS level 3 specification in iUML-B and Event-B. Int. J. Softw. Tools Technol. Transf. 22(3), 297\u2013313 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00548-w","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1276_CR16","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/s10009-020-00551-6","volume":"22","author":"D Hansen","year":"2020","unstructured":"Hansen, D., Leuschel, M., K\u00f6rner, P., Krings, S., Naulin, T., Nayeri, N., Schneider, D., Skowron, F.: Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. Int. J. Softw. Tools Technol. Transf. 22(3), 315\u2013332 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00551-6","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1276_CR17","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10009-019-00543-1","volume":"22","author":"A Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M., Tueno Fotso, S.J., Laleau, R.: A formal refinement-based analysis of the hybrid ERTMS\/ETCS level 3 standard. Int. J. Softw. Tools Technol. Transf. 22(3), 333\u2013347 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00543-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1276_CR18","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-019-00542-2","volume":"22","author":"SJ Tueno Fotso","year":"2020","unstructured":"Tueno Fotso, S.J., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS\/ETCS level 3 standard using a formal requirements engineering approach. Int. J. Softw. Tools Technol. Transf. 22(3), 349\u2013363 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00542-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"11","key":"1276_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-015-5346-2","volume":"58","author":"E Ahmad","year":"2015","unstructured":"Ahmad, E., Dong, Y., Larson, B.R., L\u00fc, J., Tang, T., Zhan, N.: Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL. Sci. China Inf. Sci. 58(11), 1\u201320 (2015). https:\/\/doi.org\/10.1007\/s11432-015-5346-2","journal-title":"Sci. China Inf. Sci."},{"key":"1276_CR20","doi-asserted-by":"publisher","unstructured":"SAE International: Architecture analysis & design language (AADL), (2022). https:\/\/doi.org\/10.4271\/AS5506D","DOI":"10.4271\/AS5506D"},{"key":"1276_CR21","first-page":"171","volume-title":"A Classical Mind: Essays in Honour of C.A.R. Hoare","author":"H Jifeng","year":"1994","unstructured":"Jifeng, H.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 171\u2013189. Prentice Hall, Hoboken (1994)"},{"key":"1276_CR22","doi-asserted-by":"publisher","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M.J., Conchon, S., Za\u00efdi, F. (eds.) Proceedings of the 17th International Conference on Formal Engineering Methods (ICFEM\u201915). LNCS, vol. 9407, pp. 382\u2013399. Springer, (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25","DOI":"10.1007\/978-3-319-25423-4_25"},{"key":"1276_CR23","doi-asserted-by":"publisher","unstructured":"Zhan, B., Lv, Y., Wang, S., Zhao, G., Hao, J., Ye, H., Xia, B.: Compositional verification of interacting systems using event monads. In: Andronick, J., de Moura, L. (eds.) Proceedings of the 13th International Conference on Interactive Theorem Proving (ITP\u201922). LIPIcs, vol. 237, pp. 33:1\u201333:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.33","DOI":"10.4230\/LIPIcs.ITP.2022.33"},{"key":"1276_CR24","doi-asserted-by":"publisher","unstructured":"Basile, D., Fantechi, A., Rucher, L., Mand\u00f2, G.: Analysing an autonomous tramway positioning system with the Uppaal statistical model checker. Form. Asp. Comput. 33(6), 957\u2013987 (2021). https:\/\/doi.org\/10.1007\/s00165-021-00556-1","DOI":"10.1007\/s00165-021-00556-1"},{"key":"1276_CR25","doi-asserted-by":"publisher","unstructured":"Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201920). LNCS, vol. 12327, pp. 3\u201369. Springer, (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"1276_CR26","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., Keiren, J.J.A., Lecomte, T., Leuschel, M., Rozier, K.Y., Sampaio, A., Seceleanu, C., Thomas, M., Willemse, T.A.C., Zhang, L.: Formal methods in industry. Form. Asp. Comput. 37(1), 7:1\u20137:38 (2025). https:\/\/doi.org\/10.1145\/3689374","DOI":"10.1145\/3689374"},{"key":"1276_CR27","doi-asserted-by":"publisher","unstructured":"Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P.J., L\u00fcttgen, G., Simons, A.J.H., Vilkomir, S.A., Woodward, M.R., Zedan, H.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1\u20139:76 (2009). https:\/\/doi.org\/10.1145\/1459352.1459354","DOI":"10.1145\/1459352.1459354"},{"key":"1276_CR28","first-page":"84","volume-title":"Software engineering techniques","author":"EW Dijkstra","year":"1969","unstructured":"Dijkstra, E.W.: Structured programming. In: Buxton, J.N., Randell, B. (eds.) Software engineering techniques, pp. 84\u201388. NATO Science Committee, Belgium (1969)"},{"key":"1276_CR29","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1276_CR30","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"1276_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0089-2","volume-title":"Automated Theorem Proving","author":"M Newborn","year":"2001","unstructured":"Newborn, M.: Automated Theorem Proving. Springer, Berlin (2001). https:\/\/doi.org\/10.1007\/978-1-4613-0089-2"},{"key":"1276_CR32","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, (2001). https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"key":"1276_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"1276_CR34","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL: A proof assistant for higher-order logic. LNCS, vol. 2283. Springer, (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"1276_CR35","doi-asserted-by":"publisher","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: A hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR\u201908). LNCS, vol. 5195, pp. 171\u2013178. Springer, (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"1276_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical Foundations of Cyber-Physical Systems","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"1276_CR37","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908). LNCS, vol. 4963, pp. 337\u2013340. Springer, (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1276_CR38","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)"},{"key":"1276_CR39","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV\u00a02: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer Aided Verification (CAV\u201902). LNCS, vol. 2404, pp. 359\u2013364. Springer, (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1276_CR40","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Proceedings of the 26th International Conference on Computer Aided Verification (CAV\u201914). LNCS, vol. 8559, pp. 334\u2013342. Springer, (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"2","key":"1276_CR41","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0063-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR42","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) Revised Lectures of the 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Formal Methods for the Design of Real-Time Systems (SFM-RT\u201904). LNCS, vol. 3185, pp. 200\u2013236. Springer, (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"1276_CR43","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL\u00a04.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST\u201906), pp. 125\u2013126. IEEE, (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"1276_CR44","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for playing games!. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907). LNCS, vol. 4590, pp. 121\u2013125. Springer, (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"1276_CR45","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915). LNCS, vol. 9035, pp. 206\u2013211. Springer, (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"1276_CR46","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0361-y","DOI":"10.1007\/s10009-014-0361-y"},{"key":"1276_CR47","doi-asserted-by":"publisher","unstructured":"Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3 \u2013 A modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914). LNCS, vol. 8413, pp. 187\u2013201. Springer, (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13","DOI":"10.1007\/978-3-642-54862-8_13"},{"issue":"2","key":"1276_CR48","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89\u2013107 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0244-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-23008-0","volume-title":"Understanding Behaviour of Distributed Systems Using mCRL2","author":"M Atif","year":"2023","unstructured":"Atif, M., Groote, J.F.: Understanding Behaviour of Distributed Systems Using mCRL2. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-23008-0"},{"key":"1276_CR50","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of model checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model Checking Probabilistic Systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of model checking, pp. 963\u2013999. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"issue":"1","key":"1276_CR51","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6\u20131639 (2018). https:\/\/doi.org\/10.1145\/3158668","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"1276_CR52","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and software science: state of the art and perspectives","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.-M., Yang, J., Smolka, S.A., Grosu, R.: Statistical Model Checking. In: Steffen, B., Woeginger, G.J. (eds.) Computing and software science: state of the art and perspectives, pp. 478\u2013504. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"key":"1276_CR53","volume-title":"Introduction to Static Analysis","author":"X Rival","year":"2020","unstructured":"Rival, X., Yi, K.: Introduction to Static Analysis. MIT Press, Cambridge (2020)"},{"key":"1276_CR54","volume-title":"Principles of Abstract Interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"1276_CR55","doi-asserted-by":"publisher","unstructured":"Peleska, J.: Industrial-strength model-based testing: state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings of the 8th Workshop on Model-Based Testing (MBT\u201913). EPTCS, vol. 111, pp. 3\u201328 (2013). https:\/\/doi.org\/10.4204\/EPTCS.111.1","DOI":"10.4204\/EPTCS.111.1"},{"issue":"1","key":"1276_CR56","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/S10270-019-00773-6","volume":"19","author":"A Bucchiarone","year":"2020","unstructured":"Bucchiarone, A., Cabot, J., Paige, R.F., Pierantonio, A.: Grand challenges in model-driven engineering: an analysis of the state of the research. Softw. Syst. Model. 19(1), 5\u201313 (2020). https:\/\/doi.org\/10.1007\/S10270-019-00773-6","journal-title":"Softw. Syst. Model."},{"key":"1276_CR57","doi-asserted-by":"publisher","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE\u201905), pp. 263\u2013272. ACM, (2005). https:\/\/doi.org\/10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"key":"1276_CR58","volume-title":"Fuzzing: Brute Force Vulnerability Discovery","author":"M Sutton","year":"2007","unstructured":"Sutton, M., Greene, A., Amini, P.: Fuzzing: Brute Force Vulnerability Discovery. Addison-Wesley, Boston (2007)"},{"key":"1276_CR59","doi-asserted-by":"publisher","unstructured":"Ferrari, A., ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55(4), 69:1\u201369:37 (2023). https:\/\/doi.org\/10.1145\/3520480","DOI":"10.1145\/3520480"},{"key":"1276_CR60","unstructured":"Kitchenham, B.: Procedures for performing systematic reviews. Technical Report TR\/SE-0401, Keele University. (2004)"},{"key":"1276_CR61","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.infsof.2015.03.007","volume":"64","author":"K Petersen","year":"2015","unstructured":"Petersen, K., Vakkalanka, S., Kuzniarz, L.: Guidelines for conducting systematic mapping studies in software engineering: An update. Inf. Softw. Technol. 64, 1\u201318 (2015). https:\/\/doi.org\/10.1016\/j.infsof.2015.03.007","journal-title":"Inf. Softw. Technol."},{"key":"1276_CR62","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F., Piattino, A., Trentini, D., Ferrari, A.: On the industrial uptake of formal methods in the railway domain: a survey with stakeholders. In: Furia, C.A., Winter, K. (eds.) Proceedings of the 14th International Conference on Integrated Formal Methods (iFM\u201918). LNCS, vol. 11023, pp. 20\u201329. Springer, (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_2","DOI":"10.1007\/978-3-319-98938-9_2"},{"key":"1276_CR63","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Bor\u00e4lv, A., Fantechi, A., Ferrari, A., Gnesi, S., L\u00f6fving, C., Mazzanti, F.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Proceedings of the 3rd World Congress on Formal Methods: The Next 30 Years (FM\u201919). LNCS, vol. 11800, pp. 762\u2013772. Springer, (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_46","DOI":"10.1007\/978-3-030-30942-8_46"},{"issue":"3","key":"1276_CR64","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-018-0488-3","volume":"20","author":"F Mazzanti","year":"2018","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transf. 20(3), 263\u2013288 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0488-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR65","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the 42nd ACM\/IEEE International Conference on Software Engineering (ICSE\u201920), pp. 62\u201374. ACM, (2020). https:\/\/doi.org\/10.1145\/3377811.3380373","DOI":"10.1145\/3377811.3380373"},{"issue":"11","key":"1276_CR66","doi-asserted-by":"publisher","first-page":"4675","DOI":"10.1109\/TSE.2021.3124677","volume":"48","author":"A Ferrari","year":"2022","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H.: Systematic evaluation and usability analysis of formal methods tools for railway signaling system design. IEEE Trans. Softw. Eng. 48(11), 4675\u20134691 (2022). https:\/\/doi.org\/10.1109\/TSE.2021.3124677","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1276_CR67","unstructured":"Lano, K.: The B Language and Method: a Guide to Practical Formal Development. FACIT. Springer, (1996). https:\/\/link.springer.com\/book\/10.1007\/978-1-4471-1494-9"},{"issue":"1\u20132","key":"1276_CR68","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundam. Inform. 77(1\u20132), 1\u201328 (2007)","journal-title":"Fundam. Inform."},{"key":"1276_CR69","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010). https:\/\/doi.org\/10.1017\/CBO9781139195881"},{"key":"1276_CR70","doi-asserted-by":"publisher","unstructured":"Chiappini, A., Cimatti, A., Macchi, L., Rebollo, O., Roveri, M., Susi, A., Tonetta, S., Vittorini, B.: Formalization and validation of a subset of the European Train Control System. In: Proceedings of the 32nd International Conference on Software Engineering (ICSE\u201910), pp. 109\u2013118. ACM, (2010). https:\/\/doi.org\/10.1145\/1810295.1810312","DOI":"10.1145\/1810295.1810312"},{"issue":"2","key":"1276_CR71","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s10270-009-0130-7","volume":"10","author":"A Cimatti","year":"2011","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Formalizing requirements with object models and temporal constraints. Softw. Syst. Model. 10(2), 147\u2013160 (2011). https:\/\/doi.org\/10.1007\/s10270-009-0130-7","journal-title":"Softw. Syst. Model."},{"key":"1276_CR72","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Validation of requirements for hybrid systems: a formal approach. ACM Trans. Softw. Eng. Methodol. 21(4), 22:1\u201322:34 (2012). https:\/\/doi.org\/10.1145\/2377656.2377659","DOI":"10.1145\/2377656.2377659"},{"key":"1276_CR73","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/j.is.2014.11.007","volume":"49","author":"M Bosschaart","year":"2015","unstructured":"Bosschaart, M., Quaglietta, E., Janssen, B., Goverde, R.M.P.: Efficient formalization of railway interlocking data in RailML. Inf. Syst. 49, 126\u2013141 (2015). https:\/\/doi.org\/10.1016\/j.is.2014.11.007","journal-title":"Inf. Syst."},{"key":"1276_CR74","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.jss.2016.09.027","volume":"122","author":"B Hamid","year":"2016","unstructured":"Hamid, B., P\u00e9rez, J.: Supporting pattern-based dependability engineering via model-driven development: approach, tool-support and empirical validation. J. Syst. Softw. 122, 239\u2013273 (2016). https:\/\/doi.org\/10.1016\/j.jss.2016.09.027","journal-title":"J. Syst. Softw."},{"issue":"1","key":"1276_CR75","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10270-016-0517-1","volume":"17","author":"D Wu","year":"2018","unstructured":"Wu, D., Schnieder, E.: Scenario-based system design with colored Petri nets: an application to train control systems. Softw. Syst. Model. 17(1), 295\u2013317 (2018). https:\/\/doi.org\/10.1007\/s10270-016-0517-1","journal-title":"Softw. Syst. Model."},{"key":"1276_CR76","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2020.101833","author":"CF Snook","year":"2021","unstructured":"Snook, C.F., Hoang, T.S., Dghaym, D., Salehi Fathabadi, A., Butler, M.J.: Domain-specific scenarios for refinement-based methods. J. Syst. Archit. (2021). https:\/\/doi.org\/10.1016\/j.sysarc.2020.101833","journal-title":"J. Syst. Archit."},{"key":"1276_CR77","doi-asserted-by":"publisher","unstructured":"Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S.A. (eds.) Proceedings of the 4th International Conference of B and Z Users (ZB\u201905). LNCS, vol. 3455, pp. 334\u2013354. Springer, (2005). https:\/\/doi.org\/10.1007\/11415787_20","DOI":"10.1007\/11415787_20"},{"issue":"6","key":"1276_CR78","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-010-0172-1","volume":"23","author":"M Leuschel","year":"2011","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Form. Asp. Comput. 23(6), 683\u2013709 (2011). https:\/\/doi.org\/10.1007\/s00165-010-0172-1","journal-title":"Form. Asp. Comput."},{"key":"1276_CR79","doi-asserted-by":"publisher","unstructured":"Abo, R., Voisin, L.: Formal Implementation of data validation for railway safety-related systems with OVADO. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) Proceedings of the SEFM 2013 Collocated Workshops: BEAT2, WS-FMDS, FM-RAIL-Bok, MoKMaSD, and OpenCert. LNCS, vol. 8368, pp. 221\u2013236. Springer, (2013). https:\/\/doi.org\/10.1007\/978-3-319-05032-4_17","DOI":"10.1007\/978-3-319-05032-4_17"},{"issue":"6","key":"1276_CR80","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1007\/s10009-014-0304-7","volume":"16","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nga, N.H., Roggenbach, M., Schneider, S.A., Treharne, H.: Techniques for modelling and verifying railway interlockings. Int. J. Softw. Tools Technol. Transf. 16(6), 685\u2013711 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0304-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR81","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.scico.2016.04.010","volume":"131","author":"A F\u00fcrst","year":"2016","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D.A., Sato, N., Miyazaki, K.: Large-scale system development using abstract data types and refinement. Sci. Comput. Program. 131, 59\u201375 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.04.010","journal-title":"Sci. Comput. Program."},{"key":"1276_CR82","doi-asserted-by":"publisher","unstructured":"Reichl, K., Fischer, T., Tummeltshammer, P.: Using formal methods for verification and validation in railway. In: Aichernig, B.K., Furia, C.A. (eds.) Proceedings of the 10th International Conference on Tests and Proofs (TAP\u201916). LNCS, vol. 9762, pp. 3\u201313. Springer, (2016). https:\/\/doi.org\/10.1007\/978-3-319-41135-4_1","DOI":"10.1007\/978-3-319-41135-4_1"},{"key":"1276_CR83","doi-asserted-by":"publisher","unstructured":"Comptier, M., D\u00e9harbe, D., Molinero Perez, J., Mussat, L., Thibaut, P., Sabatier, D.: Safety analysis of a CBTC system: a rigorous approach with Event-B. In: Fantechi, A., Lecomte, T., Romanovsky, A.B. (eds.) Proceedings of the 2nd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201917). LNCS, vol. 10598, pp. 148\u2013159. Springer, (2017). https:\/\/doi.org\/10.1007\/978-3-319-68499-4_10","DOI":"10.1007\/978-3-319-68499-4_10"},{"key":"1276_CR84","doi-asserted-by":"publisher","unstructured":"Idani, A., Ledru, Y., Ait Wakrime, A., Ben Ayed, R., Collart Dutilleul, S.: Incremental development of a safety critical system combining formal methods and DSMLs: application to a railway system. In: Larsen, K.G., Willemse, T.A.C. (eds.) Proceedings of the 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201919). LNCS, vol. 11687, pp. 93\u2013109. Springer, (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_6","DOI":"10.1007\/978-3-030-27008-7_6"},{"key":"1276_CR85","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.scico.2017.10.011","volume":"154","author":"U Berger","year":"2018","unstructured":"Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Verification of the European rail traffic management system in real-time Maude. Sci. Comput. Program. 154, 61\u201388 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.10.011","journal-title":"Sci. Comput. Program."},{"issue":"12","key":"1276_CR86","doi-asserted-by":"publisher","first-page":"1989","DOI":"10.1109\/TCAD.2017.2681076","volume":"36","author":"Y Bao","year":"2017","unstructured":"Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking. IEEE Trans. Comput. Aided. Des. Integr. Circuits Syst. 36(12), 1989\u20132002 (2017). https:\/\/doi.org\/10.1109\/TCAD.2017.2681076","journal-title":"IEEE Trans. Comput. Aided. Des. Integr. Circuits Syst."},{"issue":"3","key":"1276_CR87","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/MITS.2018.2842230","volume":"10","author":"Y Wang","year":"2018","unstructured":"Wang, Y., Chen, L., Kirkwood, D., Fu, P., Lv, J., Roberts, C.: Hybrid online model-based testing for communication-based train control systems. IEEE Intell. Transp. Syst. Mag. 10(3), 35\u201347 (2018). https:\/\/doi.org\/10.1109\/MITS.2018.2842230","journal-title":"IEEE Intell. Transp. Syst. Mag."},{"issue":"3","key":"1276_CR88","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1049\/cce:19970304","volume":"8","author":"B Kitchenham","year":"1997","unstructured":"Kitchenham, B., Linkman, S., Law, D.: DESMET: a methodology for evaluating software engineering methods and tools. Comput. Control. Eng. J. 8(3), 120\u2013126 (1997). https:\/\/doi.org\/10.1049\/cce:19970304","journal-title":"Comput. Control. Eng. J."},{"key":"1276_CR89","doi-asserted-by":"publisher","unstructured":"Ferrari, A., ter Beek, M.H., Mazzanti, F., Basile, D., Fantechi, A., Gnesi, S., Piattino, A., Trentini, D.: Survey on formal methods and tools in railways: the ASTRail approach. In: Collart Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) Proceedings of the 3rd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201919). LNCS, vol. 11495, pp. 226\u2013241. Springer, (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_15","DOI":"10.1007\/978-3-030-18744-6_15"},{"key":"1276_CR90","unstructured":"Dabney, J.B., Harman, T.L.: Mastering Simulink. Pearson, (2003). https:\/\/www.pearson.com\/en-us\/subject-catalog\/p\/mastering-simulink\/P200000003257\/9780131424777"},{"issue":"3\u20134","key":"1276_CR91","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3\u20134), 213\u2013254 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0038-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR92","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Owre, S., Rue\u00df, H., Rushby, J.M., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201904). LNCS, vol. 3114, pp. 496\u2013500. Springer, (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_45","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"1276_CR93","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, (2002). https:\/\/www.pearson.com\/en-us\/subject-catalog\/p\/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers\/P200000009296\/9780321143068"},{"issue":"2","key":"1276_CR94","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2010.07.002","volume":"76","author":"MH ter Beek","year":"2011","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state\/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119\u2013135 (2011). https:\/\/doi.org\/10.1016\/j.scico.2010.07.002","journal-title":"Sci. Comput. Program."},{"key":"1276_CR95","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12578-2","volume-title":"Requirements Engineering: Fundamentals, Principles, and Techniques","author":"K Pohl","year":"2010","unstructured":"Pohl, K.: Requirements Engineering: Fundamentals, Principles, and Techniques. Springer, Berlin (2010)"},{"issue":"2","key":"1276_CR96","doi-asserted-by":"publisher","first-page":"233","DOI":"10.17730\/humo.56.2.x335923511444655","volume":"56","author":"R Scupin","year":"1997","unstructured":"Scupin, R.: The KJ method: A technique for analyzing data derived from Japanese ethnology. Hum. Organ. 56(2), 233\u2013237 (1997). https:\/\/doi.org\/10.17730\/humo.56.2.x335923511444655","journal-title":"Hum. Organ."},{"key":"1276_CR97","doi-asserted-by":"publisher","unstructured":"Brooke, J.: SUS: A \u2018quick and dirty\u2019 usability scale. In: Jordan, P.W., Thomas, B., Weerdmeester, B.A., McClelland, I.L. (eds.) Usability Evaluation in Industry, pp. 189\u2013194. CRC, (1996). Chap. 21. https:\/\/doi.org\/10.1201\/9781498710411","DOI":"10.1201\/9781498710411"},{"issue":"2","key":"1276_CR98","doi-asserted-by":"publisher","first-page":"29","DOI":"10.5555\/2817912.2817913","volume":"8","author":"J Brooke","year":"2013","unstructured":"Brooke, J.: SUS: A retrospective. J. Usability Stud. 8(2), 29\u201340 (2013). https:\/\/doi.org\/10.5555\/2817912.2817913","journal-title":"J. Usability Stud."},{"issue":"6","key":"1276_CR99","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1080\/10447310802205776","volume":"24","author":"A Bangor","year":"2008","unstructured":"Bangor, A., Kortum, P.T., Miller, J.T.: An empirical evaluation of the system usability scale. Int. J. Hum. Comput. Interact. 24(6), 574\u2013594 (2008). https:\/\/doi.org\/10.1080\/10447310802205776","journal-title":"Int. J. Hum. Comput. Interact."},{"key":"1276_CR100","unstructured":"Furness, N., van Houten, H., Arenas, L., Bartholomeus, M.: ERTMS level 3: the game-changer. IRSE News 232, 2\u20139 (2017). https:\/\/www.irse.nl\/resources\/170314-ERTMS-L3-The-gamechanger-from-IRSE-News-Issue-232.pdf"},{"issue":"10","key":"1276_CR101","doi-asserted-by":"publisher","first-page":"2602","DOI":"10.1109\/TITS.2017.2658179","volume":"18","author":"J Marais","year":"2017","unstructured":"Marais, J., Beugin, J., Berbineau, M.: A survey of GNSS-based research and developments for the European railway signaling. IEEE Trans. Intell. Transp. Syst. 18(10), 2602\u20132618 (2017). https:\/\/doi.org\/10.1109\/TITS.2017.2658179","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"3","key":"1276_CR102","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/S10009-022-00653-3","volume":"24","author":"D Basile","year":"2022","unstructured":"Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Exploring the ERTMS\/ETCS full moving block specification: an experience with formal methods. Int. J. Softw. Tools Technol. Transf. 24(3), 351\u2013370 (2022). https:\/\/doi.org\/10.1007\/S10009-022-00653-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR103","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1016\/j.trc.2017.07.002","volume":"82","author":"M Biagi","year":"2017","unstructured":"Biagi, M., Carnevali, L., Paolieri, M., Vicario, E.: Performability evaluation of the ERTMS\/ETCS - Level 3. Transp. Res. C-Emer. 82, 314\u2013336 (2017). https:\/\/doi.org\/10.1016\/j.trc.2017.07.002","journal-title":"Transp. Res. C-Emer."},{"key":"1276_CR104","doi-asserted-by":"publisher","unstructured":"Bartholomeus, M., Luttik, B., Willemse, T.: Modeling and analysing ERTMS hybrid level\u00a03 with the mCRL2 toolset. In: Howar, F., Barnat, J. (eds.) Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201918). LNCS, vol. 11119, pp. 98\u2013114. Springer, (2018). https:\/\/doi.org\/10.1007\/978-3-030-00244-2_7","DOI":"10.1007\/978-3-030-00244-2_7"},{"key":"1276_CR105","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Ciancia, V.: Statistical model checking of a moving block railway signalling scenario with Uppaal SMC: experience and outlook. In: Margaria, T., Steffen, B. (eds.) Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification (ISoLA\u201918). LNCS, vol. 11245, pp. 372\u2013391. Springer, (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_24","DOI":"10.1007\/978-3-030-03421-4_24"},{"key":"1276_CR106","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Ferrari, A., Legay, A.: Modelling and analysing ERTMS L3 moving block railway signalling with Simulink and Uppaal SMC. In: Larsen, K.G., Willemse, T. (eds.) Proceedings of the 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201919). LNCS, vol. 11687, pp. 1\u201321. Springer, (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_1","DOI":"10.1007\/978-3-030-27008-7_1"},{"key":"1276_CR107","doi-asserted-by":"publisher","unstructured":"Douglass, B.P.: Real-Time UML. In: Damm, W., Olderog, E.-R. (eds.) Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u201902). LNCS, vol. 2469, pp. 53\u201370. Springer, (2002). https:\/\/doi.org\/10.1007\/3-540-45739-9_4","DOI":"10.1007\/3-540-45739-9_4"},{"key":"1276_CR108","doi-asserted-by":"publisher","unstructured":"Selic, B.: The real-time UML standard: definition and application. In: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE\u201902), pp. 770\u2013772 (2002). https:\/\/doi.org\/10.1109\/DATE.2002.998385","DOI":"10.1109\/DATE.2002.998385"},{"issue":"3","key":"1276_CR109","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). https:\/\/doi.org\/10.1016\/0167-6423(87)90035-9","journal-title":"Sci. Comput. Program."},{"key":"1276_CR110","doi-asserted-by":"publisher","unstructured":"Filipovikj, P., Mahmud, N., Marinescu, R., Seceleanu, C., Ljungkrantz, O., L\u00f6nn, H.: Simulink to UPPAAL statistical model checker: Analyzing Automotive Industrial Systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) Proceedings of the 21st International Symposium on Formal Methods (FM\u201916). LNCS, vol. 9995, pp. 748\u2013756. Springer, (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_46","DOI":"10.1007\/978-3-319-48989-6_46"},{"key":"1276_CR111","doi-asserted-by":"publisher","unstructured":"Jin, Y., Xie, G., Chen, P., Hei, X., Ji, W., Zhao, J.: High-speed train emergency brake modeling and online identification of time-varying parameters. Math. Probl. Eng. 2020 (2020). https:\/\/doi.org\/10.1155\/2020\/3872852","DOI":"10.1155\/2020\/3872852"},{"key":"1276_CR112","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Legay, A.: Strategy synthesis for autonomous driving in a moving block railway system with Uppaal Stratego. In: Gotsman, A., Sokolova, A. (eds.) Proceedings of the 40th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE\u201920). LNCS, vol. 12136, pp. 3\u201321. Springer, (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_1","DOI":"10.1007\/978-3-030-50086-3_1"},{"key":"1276_CR113","doi-asserted-by":"publisher","unstructured":"Jaeger, M., Jensen, P.G., Larsen, K.G., Legay, A., Sedwards, S., Taankvist, J.H.: Teaching Stratego to play ball: optimal synthesis for continuous space MDPs. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201919). LNCS, vol. 11781, pp. 81\u201397. Springer, (2019).https:\/\/doi.org\/10.1007\/978-3-030-31784-3_5","DOI":"10.1007\/978-3-030-31784-3_5"},{"issue":"3","key":"1276_CR114","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s10009-022-00657-z","volume":"24","author":"R Gu","year":"2022","unstructured":"Gu, R., Jensen, P.G., Poulsen, D.B., Seceleanu, C., Enoiu, E., Lundqvist, K.: Verifiable strategy synthesis for multiple autonomous agents: a scalable approach. Int. J. Softw. Tools Technol. Transf. 24(3), 395\u2013414 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00657-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR115","doi-asserted-by":"publisher","unstructured":"Gu, R., Jensen, P.G., Seceleanu, C., Enoiu, E., Lundqvist, K.: Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems. Sci. Comput. Program. 224 (2022). https:\/\/doi.org\/10.1016\/J.SCICO.2022.102894","DOI":"10.1016\/J.SCICO.2022.102894"},{"key":"1276_CR116","unstructured":"Gu, R.: Formal methods for scalable synthesis and verification of autonomous systems: mission planning and collision avoidance. PhD thesis, M\u00e4lardalen University, (2022). https:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:mdh:diva-58086"},{"key":"1276_CR117","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Di Giandomenico, F., Fantechi, A., Gnesi, S., Spagnolo, G.O.: 30 years of simulation-based quantitative analysis tools: a comparison experiment between M\u00f6bius and Uppaal SMC. In: Margaria, T., Steffen, B. (eds.) Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification (ISoLA\u201920). LNCS, vol. 12476, pp. 368\u2013384. Springer, (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_21","DOI":"10.1007\/978-3-030-61362-4_21"},{"key":"1276_CR118","doi-asserted-by":"publisher","unstructured":"Clark, G., Courtney, T., Daly, D., Deavours, D., Derisavi, S., Doyle, J.M., Sanders, W.H., Webster, P.: The M\u00f6bius modeling tool. In: Proceedings of the 9th International Workshop on Petri Nets and Performance Models (PNPM\u201901), pp. 241\u2013250. IEEE, (2001). https:\/\/doi.org\/10.1109\/PNPM.2001.953373","DOI":"10.1109\/PNPM.2001.953373"},{"issue":"2","key":"1276_CR119","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.jrtpm.2016.03.003","volume":"6","author":"D Basile","year":"2016","unstructured":"Basile, D., Chiaradonna, S., Di Giandomenico, F., Gnesi, S.: A stochastic model-based approach to analyse reliable energy-saving rail road switch heating systems. J. Rail Transp. Plan. Manag. 6(2), 163\u2013181 (2016). https:\/\/doi.org\/10.1016\/j.jrtpm.2016.03.003","journal-title":"J. Rail Transp. Plan. Manag."},{"key":"1276_CR120","doi-asserted-by":"publisher","unstructured":"Basile, D., Di Giandomenico, F., Gnesi, S.: Statistical model checking of an energy-saving cyber-physical system in the railway domain. In: Proceedings of the 32nd Symposium on Applied Computing (SAC\u201917), pp. 1356\u20131363. ACM, (2017). https:\/\/doi.org\/10.1145\/3019612.3019824","DOI":"10.1145\/3019612.3019824"},{"key":"1276_CR121","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Ciancia, V., Latella, D., Massink, M., Spagnolo, G.O.: Spatial model checking for smart stations: research challenges. In: Lluch Lafuente, A., Mavridou, A. (eds.) Proceedings of the 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201921). LNCS, vol. 12863, pp. 39\u201347. Springer, (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_3","DOI":"10.1007\/978-3-030-85248-1_3"},{"key":"1276_CR122","doi-asserted-by":"publisher","unstructured":"Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: A spatial model checker for declarative image analysis. In: Vojnar, T., Zhang, L. (eds.) Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919). LNCS, vol. 11427, pp. 281\u2013298. Springer, (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_16","DOI":"10.1007\/978-3-030-17462-0_16"},{"key":"1276_CR123","doi-asserted-by":"publisher","unstructured":"Ciancia, V., Belmonte, G., Latella, D., Massink, M.: A hands-on introduction to spatial model checking using VoxLogicA. In: Laarman, A., Sokolova, A. (eds.) Proceedings of the 27th International Symposium on Model Checking Software (SPIN\u201921). LNCS, vol. 12864, pp. 22\u201341. Springer, (2021). https:\/\/doi.org\/10.1007\/978-3-030-84629-9_2","DOI":"10.1007\/978-3-030-84629-9_2"},{"key":"1276_CR124","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H.: Contract automata library. Sci. Comput. Program. 221 (2022). https:\/\/doi.org\/10.1016\/j.scico.2022.102841","DOI":"10.1016\/j.scico.2022.102841"},{"issue":"5","key":"1276_CR125","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/S10009-023-00730-1","volume":"25","author":"D Basile","year":"2023","unstructured":"Basile, D., ter Beek, M.H., Bussi, L., Ciancia, V.: A toolchain for strategy synthesis with spatial properties. Int. J. Softw. Tools Technol. Transf. 25(5), 641\u2013658 (2023). https:\/\/doi.org\/10.1007\/S10009-023-00730-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1276_CR126","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Carnevali, L., Chiaradonna, S., Di Giandomenico, F., Fantechi, A., Gori, G.: An integrated perspective on the evaluation of complex railway systems. In: Margaria, T., Steffen, B. (eds.) Proceedings of the 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA\u201924). LNCS, vol. 15223, pp. 190\u2013207. Springer, (2024). https:\/\/doi.org\/10.1007\/978-3-031-75390-9_13","DOI":"10.1007\/978-3-031-75390-9_13"},{"key":"1276_CR127","doi-asserted-by":"publisher","unstructured":"Tang, R., De Donato, L., Be\u0161inovi\u0107, N., Flammini, F., Goverde, R.M.P., Lin, Z., Liu, R., Tang, T., Vittorini, V., Wang, Z.: A literature review of artificial intelligence applications in railway systems. Transp. Res. C-Emer. 140 (2022). https:\/\/doi.org\/10.1016\/j.trc.2022.103679","DOI":"10.1016\/j.trc.2022.103679"},{"issue":"2","key":"1276_CR128","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1109\/EMR.2023.3262282","volume":"51","author":"M Binder","year":"2023","unstructured":"Binder, M., Mezhuyev, V., Tschandl, M.: Predictive maintenance for railway domain: a systematic literature review. IEEE Eng. Manag. Rev. 51(2), 120\u2013140 (2023). https:\/\/doi.org\/10.1109\/EMR.2023.3262282","journal-title":"IEEE Eng. Manag. Rev."},{"key":"1276_CR129","doi-asserted-by":"publisher","unstructured":"Fidma, M.A., Hamour, N., Ouchani, S., Benslimane, S.M.: Predictive maintenance approaches in Industry\u00a04.0: a systematic literature review. In: Proceedings of the 31st IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE\u201923), pp. 1\u20136. IEEE, (2023). https:\/\/doi.org\/10.1109\/WETICE57085.2023.10477802","DOI":"10.1109\/WETICE57085.2023.10477802"},{"key":"1276_CR130","doi-asserted-by":"publisher","unstructured":"Hafsi, M., Hamour, N., Ouchani, S.: Predictive maintenance for smart industrial systems: a roadmap. In: Procedia Comput. Sci. 220, 645\u2013650 (2023). Proceedings of the 6th International Conference on Emerging Data and Industry 4.0 (EDI40\u201923). https:\/\/doi.org\/10.1016\/J.PROCS.2023.03.082","DOI":"10.1016\/J.PROCS.2023.03.082"},{"key":"1276_CR131","doi-asserted-by":"publisher","unstructured":"Longo, N., Serpi, V., Jacazio, G., Sorli, M.: Model-based predictive maintenance techniques applied to automotive industry. In: Proceedings of the 4th European Conference of the Prognostics and Health Management Society (PHME\u201918), vol. 4. PHM Society, (2018). https:\/\/doi.org\/10.36001\/phme.2018.v4i1.353","DOI":"10.36001\/phme.2018.v4i1.353"},{"key":"1276_CR132","doi-asserted-by":"publisher","unstructured":"Meghoe, A.A.: Physical model-based predictive maintenance for rail infrastructure. PhD thesis, University of Twente, (2019). https:\/\/doi.org\/10.3990\/1.9789036548786","DOI":"10.3990\/1.9789036548786"},{"issue":"3","key":"1276_CR133","doi-asserted-by":"publisher","first-page":"2213","DOI":"10.1109\/JSYST.2019.2905565","volume":"13","author":"W Zhang","year":"2019","unstructured":"Zhang, W., Yang, D., Wang, H.: Data-driven methods for predictive maintenance of industrial equipment: a survey. IEEE Syst. J. 13(3), 2213\u20132227 (2019). https:\/\/doi.org\/10.1109\/JSYST.2019.2905565","journal-title":"IEEE Syst. J."},{"key":"1276_CR134","doi-asserted-by":"publisher","unstructured":"Cao, Q., Zanni-Merk, C., Samet, A., Reich, C., Beckmann, A., Giannetti, C., de Beuvron, F.: KSPMI: A knowledge-based system for predictive maintenance in Industry 4.0. Robot. Comput.-Integr Manuf. 74 (2022). https:\/\/doi.org\/10.1016\/J.RCIM.2021.102281","DOI":"10.1016\/J.RCIM.2021.102281"},{"key":"1276_CR135","doi-asserted-by":"publisher","unstructured":"van Dinter, R., Tekinerdogan, B., Catal, C.: Predictive maintenance using digital twins: a systematic literature review. Inf. Softw. Technol. 151 (2022). https:\/\/doi.org\/10.1016\/J.INFSOF.2022.107008","DOI":"10.1016\/J.INFSOF.2022.107008"},{"key":"1276_CR136","doi-asserted-by":"publisher","unstructured":"Ferdous, R., Spagnolo, G., Borselli, A., Rota, L., Ferrari, A.: Identifying maintenance needs with machine learning: a case study in railways. In: Proceedings of the 32nd International Requirements Engineering Conference Workshops (REW\u201924), pp. 22\u201325. IEEE, (2024). https:\/\/doi.org\/10.1109\/REW61692.2024.00008","DOI":"10.1109\/REW61692.2024.00008"},{"issue":"1\u20134","key":"1276_CR137","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s00170-012-4303-0","volume":"66","author":"L Cauffriez","year":"2013","unstructured":"Cauffriez, L., Loslever, P., Caouder, N., Turgis, F., Copin, R.: Robustness study and reliability growth based on exploratory design of experiments and statistical analysis: a case study using a train door test bench. J. Adv. Manuf. Technol. 66(1\u20134), 27\u201344 (2013). https:\/\/doi.org\/10.1007\/s00170-012-4303-0","journal-title":"J. Adv. Manuf. Technol."},{"key":"1276_CR138","doi-asserted-by":"publisher","unstructured":"Parri, J., Sampietro, S., Vicario, E.: FaultFlow: a tool supporting an MDE approach for timed failure logic analysis. In: Proceedings of the 17th European Dependable Computing Conference (EDCC\u201921), pp. 25\u201332. IEEE, (2021). https:\/\/doi.org\/10.1109\/EDCC53658.2021.00011","DOI":"10.1109\/EDCC53658.2021.00011"},{"key":"1276_CR139","doi-asserted-by":"publisher","unstructured":"Seisenberger, M., ter Beek, M.H., Fan, X., Ferrari, A., Haxthausen, A.E., James, P., Lawrence, A., Luttik, B., van de Pol, J., Wimmer, S.: Safe and secure future AI-driven railway technologies: challenges for formal methods in railway. In: Margaria, T., Steffen, B. (eds.) Proceedings of the 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Practice (ISoLA\u201922). LNCS, vol. 13704, pp. 246\u2013268. Springer, (2022). https:\/\/doi.org\/10.1007\/978-3-031-19762-8_20","DOI":"10.1007\/978-3-031-19762-8_20"},{"issue":"6","key":"1276_CR140","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1007\/S10270-023-01124-2","volume":"22","author":"M Gleirscher","year":"2023","unstructured":"Gleirscher, M., van de Pol, J., Woodcock, J.: A manifesto for applicable formal methods. Softw. Syst. Model. 22(6), 1737\u20131749 (2023). https:\/\/doi.org\/10.1007\/S10270-023-01124-2","journal-title":"Softw. Syst. Model."},{"key":"1276_CR141","doi-asserted-by":"publisher","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: Chockler, H., Weissenbacher, G. (eds.) Proceedings of the 30th International Conference on Computer Aided Verification (CAV\u201918). LNCS, vol. 10982, pp. 467\u2013486. Springer, (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_28","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"1276_CR142","doi-asserted-by":"publisher","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K.S., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using SMT. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201918), pp. 1\u20139. IEEE, (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"1276_CR143","doi-asserted-by":"publisher","unstructured":"Rungta, N.: A Billion SMT Queries a Day. In: Shoham, S., Vizel, Y. (eds.) Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922). LNCS, vol. 13371, pp. 3\u201318. Springer, (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"1276_CR144","unstructured":"Cook, B.: Automated reasoning\u2019s scientific frontiers (2022). https:\/\/www.amazon.science\/blog\/automated-reasonings-scientific-frontiers"},{"key":"1276_CR145","unstructured":"Binns, L.: By computers, for computers: Improving scanner metrology software with generated code (2023). https:\/\/www.linkedin.com\/pulse\/computers-improving-scanner-metrology-software-code-lewis\/"},{"key":"1276_CR146","doi-asserted-by":"publisher","unstructured":"ter Beek, M., Broy, M., Dongol, B.: The Role of Formal Methods in Computer Science Education. Inroads 15(4), 58\u201366 (2024). https:\/\/doi.org\/10.1145\/3702231","DOI":"10.1145\/3702231"},{"key":"1276_CR147","doi-asserted-by":"publisher","unstructured":"Dongol, B., Dubois, C., Hallerstede, S., Hehner, E., Morgan, C., M\u00fcller, P., Ribeiro, L., Silva, A., Smith, G., de Vink, E.: On formal methods thinking in computer science education. Form. Asp. Comput. 37(1), 8:1\u20138:23 (2025). https:\/\/doi.org\/10.1145\/3670419","DOI":"10.1145\/3670419"},{"issue":"4","key":"1276_CR148","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1232743.1232745","volume":"50","author":"J Kramer","year":"2007","unstructured":"Kramer, J.: Is abstraction the Key to computing? Commun. ACM 50(4), 36\u201342 (2007). https:\/\/doi.org\/10.1145\/1232743.1232745","journal-title":"Commun. ACM"},{"key":"1276_CR149","doi-asserted-by":"publisher","unstructured":"Khelladi, D.E., Combemale, B., Acher, M., Barais, O.: On the power of abstraction: a model-driven co-evolution approach of software code. In: Proceedings of the 42nd International Conference on Software Engineering Track on New Ideas and Emerging Results (ICSE-NIER\u201920), pp. 85\u201388. ACM, (2020). https:\/\/doi.org\/10.1145\/3377816.3381727","DOI":"10.1145\/3377816.3381727"},{"key":"1276_CR150","doi-asserted-by":"publisher","unstructured":"Benjamin, P.C., Erraguntla, M., Delen, D., Mayer, R.J.: Simulation modeling at multiple levels of abstraction. In: Proceedings of the 30th Winter Simulation Conference (WSC\u201998), pp. 391\u2013398. IEEE, (1998). https:\/\/doi.org\/10.1109\/WSC.1998.745013","DOI":"10.1109\/WSC.1998.745013"},{"key":"1276_CR151","doi-asserted-by":"publisher","unstructured":"Franceschini, R., Challenger, M., Cicchetti, A., Denil, J., Vangheluwe, H.: Challenges for automation in adaptive abstraction. In: Companion Proceedings of the 22nd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS-C\u201919), pp. 443\u2013448. IEEE, (2019). https:\/\/doi.org\/10.1109\/MODELS-C.2019.00071","DOI":"10.1109\/MODELS-C.2019.00071"},{"key":"1276_CR152","doi-asserted-by":"publisher","unstructured":"Broy, M., Brucker, A.D., Fantechi, A., Gleirscher, M., Havelund, K., Kuppe, M.A., Mendes, A., Platzer, A., Ringert, J.O., Sullivan, A.: Does every computer scientist need to know formal methods? Form. Asp. Comput. 37(1), 6:1\u20136:17 (2025). https:\/\/doi.org\/10.1145\/3670795","DOI":"10.1145\/3670795"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01276-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-025-01276-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01276-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T02:20:11Z","timestamp":1763173211000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-025-01276-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,28]]},"references-count":152,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["1276"],"URL":"https:\/\/doi.org\/10.1007\/s10270-025-01276-3","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2,28]]},"assertion":[{"value":"16 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 August 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 January 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 February 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}