{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:16:00Z","timestamp":1757618160478,"version":"3.44.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T00:00:00Z","timestamp":1748908800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T00:00:00Z","timestamp":1748908800000},"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":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,9]]},"DOI":"10.1007\/s11334-025-00602-8","type":"journal-article","created":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T16:10:36Z","timestamp":1748967036000},"page":"985-1007","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Visual animation of B specifications using executable DSLs"],"prefix":"10.1007","volume":"21","author":[{"given":"Asfand","family":"Yar","sequence":"first","affiliation":[]},{"given":"Akram","family":"Idani","sequence":"additional","affiliation":[]},{"given":"Yves","family":"Ledru","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Collart-Dutilleul","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,3]]},"reference":[{"key":"602_CR1","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/52.391826","volume":"12","author":"JP Bowen","year":"1995","unstructured":"Bowen JP, Hinchey MG (1995) Seven more myths of formal methods. IEEE Softw 12:34\u201341","journal-title":"IEEE Softw"},{"key":"602_CR2","doi-asserted-by":"crossref","unstructured":"Gaudel MC (1991) Advantages and limits of formal approaches for ultra-high dependability. In Proceedings of the 6th international workshop on software specification and design, IWSSD \u201991, 237\u2013241 (IEEE Computer Society Press, Washington, DC, USA, )","DOI":"10.1109\/IWSSD.1991.213054"},{"key":"602_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial J-R (1996) The B-Book: Assigning Programs to Meanings. Cambridge University Press, USA"},{"key":"602_CR4","doi-asserted-by":"crossref","unstructured":"Andova S, van\u00a0den Brand M, Engelen L, Verhoeff T (2012) MDE basics with a DSL focus. In Formal methods for model-driven engineering - 12th international school on formal methods for the design of computer, communication, and software systems, vol. 7320 of LNCS, 21\u201357 (Springer, )","DOI":"10.1007\/978-3-642-30982-3_2"},{"key":"602_CR5","doi-asserted-by":"crossref","unstructured":"Ladenberger L, Bendisposto J, Leuschel M (2009) Visualising Event-B models with B-Motion Studio. In: Alpuente M, Cook B, Joubert C (eds) Formal Methods for Industrial Critical Systems, 202\u2013204 (Springer. Berlin Heidelberg, Berlin, Heidelberg)","DOI":"10.1007\/978-3-642-04570-7_17"},{"key":"602_CR6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.110948","volume":"178","author":"S Liu","year":"2021","unstructured":"Liu S, Miao W (2021) A formal specification animation method for operation validation. J Syst Softw 178:110948","journal-title":"J Syst Softw"},{"key":"602_CR7","doi-asserted-by":"crossref","unstructured":"Watson N, Reeves S, Masci P (2018) Integrating user design and formal models within PVSio-Web. Electr Proc Theoretical Comput Sci 284","DOI":"10.4204\/EPTCS.284.8"},{"key":"602_CR8","doi-asserted-by":"crossref","unstructured":"Servat T (2006) Brama: A new graphic animation tool for B models. In: Julliand J, Kouchnarenko O (eds) B 2007: Formal Specification and Development in B, 274\u2013276 (Springer. Berlin Heidelberg, Berlin, Heidelberg)","DOI":"10.1007\/11955757_28"},{"key":"602_CR9","doi-asserted-by":"crossref","unstructured":"Ladenberger L, Leuschel M (2016) BMotionWeb: A tool for rapid creation of formal prototypes. In De\u00a0Nicola, R. & K\u00fchn, E. (eds.) Software Engineering and Formal Methods, 403\u2013417 (Springer International Publishing, Cham, )","DOI":"10.1007\/978-3-319-41591-8_27"},{"key":"602_CR10","doi-asserted-by":"crossref","unstructured":"Werth M, Leuschel M (2020) VisB: A lightweight tool to visualize formal models with SVG graphics. In Raschke, A., M\u00e9ry, D. & Houdek, F. (eds.) Rigorous State-Based Methods, 260\u2013265 (Springer International Publishing, Cham, )","DOI":"10.1007\/978-3-030-48077-6_21"},{"key":"602_CR11","doi-asserted-by":"crossref","unstructured":"Krings S, K\u00f6rner P (2021) Prototyping games using formal methods. In Cerone, A. & Roggenbach, M. (eds.) Formal Methods \u2013 Fun for Everybody, 124\u2013142 (Springer International Publishing, Cham, )","DOI":"10.1007\/978-3-030-71374-4_6"},{"key":"602_CR12","unstructured":"Steinberg D, Budinsky F, Paternostro M, Merks E (2009) EMF: Eclipse Modeling Frameworke (Addison-Wesley, ), 2nd edn"},{"key":"602_CR13","doi-asserted-by":"crossref","unstructured":"Idani A (2020) Meeduse: A tool to build and run proved DSLs. In Dongol, B. & Troubitsyna, E. (eds.) Integrated Formal Methods, 349\u2013367 (Springer International Publishing, Cham, )","DOI":"10.1007\/978-3-030-63461-2_19"},{"key":"602_CR14","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s11334-020-00366-3","volume":"16","author":"A Idani","year":"2020","unstructured":"Idani A, Ledru Y, Vega G (2020) Alliance of model-driven engineering with a proof-based formal approach. Innov Syst Softw Eng 16:289\u2013307","journal-title":"Innov Syst Softw Eng"},{"key":"602_CR15","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2003) Prob: A model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: Formal Methods, 855\u2013874 (Springer. Berlin Heidelberg, Berlin, Heidelberg)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"602_CR16","unstructured":"Yar A, Idani A, Ledru Y, Collart-Dutilleul S (2022) Visual animation of b specifications using executable dsls. In Proceedings of the 25th international conference on model driven engineering languages and systems: companion proceedings, MODELS \u201922, 617\u2013626 (Association for Computing Machinery, New York, NY, USA, ). https:\/\/dl.acm.org\/doi\/10.1145\/3550356.3561585"},{"key":"602_CR17","unstructured":"Leuschel M, Samia M, Bendisposto J (2008) Easy graphical animation and formula visualisation for teaching B"},{"key":"602_CR18","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF00402649","volume":"4","author":"M M\u00fcllerburg","year":"1995","unstructured":"M\u00fcllerburg M, Holenderski L, Maffe\u00efs O, Merceron A, Morley M (1995) Systematic testing and formal verification to validate reactive programs. Softw Qual J 4:287\u2013307. https:\/\/doi.org\/10.1007\/BF00402649","journal-title":"Softw Qual J"},{"key":"602_CR19","unstructured":"Eclipse sirius (2022). https:\/\/www.eclipse.org\/sirius\/"},{"key":"602_CR20","unstructured":"Acceleo. https:\/\/www.eclipse.org\/acceleo\/. Accessed: 2023-02-05"},{"key":"602_CR21","volume-title":"FME 2002: Formal Methods-Getting IT Right, 21\u201340","author":"B Legeard","year":"2002","unstructured":"Legeard B, Peureux F, Utting M (2002) Automated boundary testing from Z and B. In: Eriksson L-H, Lindsay PA (eds) FME 2002: Formal Methods-Getting IT Right, 21\u201340. Springer, Berlin Heidelberg, Berlin, Heidelberg"},{"key":"602_CR22","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, Fotso SJT, Laleau R (2020) A formal refinement-based analysis of the hybrid ERTMS\/ETCS level 3 standard. Int J Softw Tools Technol Transfer 22:333\u2013347","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"602_CR23","unstructured":"Butler MJ, Raschke A, Hoang TS, Reichl K (2018) (eds.). 6th International Conference, ABZ, vol. 10817 of LNCS (Springer, )"},{"key":"602_CR24","unstructured":"The ERTMS\/ETCS signalling system. http:\/\/www.railwaysignalling.eu\/wp-content\/uploads\/2016\/09\/ERTMS_ETCS_signalling_system_revF.pdf. Accessed: 2022-03-16"},{"key":"602_CR25","doi-asserted-by":"crossref","unstructured":"Bodeveix J-P, Filali M, Lawall J, Muller G (2005) Formal methods meet domain specific languages. In Proceedings of the 5th international conference on integrated formal methods, 187\u2013206 (Springer, )","DOI":"10.1007\/11589976_12"},{"key":"602_CR26","doi-asserted-by":"publisher","first-page":"778","DOI":"10.1177\/0037549709341635","volume":"85","author":"J Rivera","year":"2009","unstructured":"Rivera J, Dur\u00e1n F, Vallecillo A (2009) Formal specification and analysis of domain specific models using Maude. Simulation 85:778\u2013792","journal-title":"Simulation"},{"key":"602_CR27","unstructured":"Zalila F, Cr\u00e9gut X, Pantel M (2016) A DSL to Feedback Formal Verification Results. In Famelis, M., Ratiu, D. & Selim, G. M.\u00a0K. (eds.) 13th Model-Driven Engineering, Verification and Validation Workshop at MODELS conference 2016 (MoDeVVa 2016), vol. 1713, 30\u201339 (CEUR-WS : Workshop proceedings, Saint Malo, France, ). https:\/\/hal.archives-ouvertes.fr\/hal-03172263"},{"key":"602_CR28","doi-asserted-by":"crossref","unstructured":"Meyers B, Vangheluwe H, Denil J, Salay R (2020) A framework for temporal verification support in domain-specific modelling. IEEE Trans Software Eng 46:362\u2013404","DOI":"10.1109\/TSE.2018.2859946"},{"key":"602_CR29","unstructured":"Tikhonova U, Manders M, Brand van den M, Andova S, Verhoeff T (2013) Applying model transformation and Event-B for specifying an industrial DSL. In Workshop on Model Driven Engineering, Verification and Validation, CEUR Workshop Proceedings, 41\u201350 (CEUR-WS.org, )"},{"key":"602_CR30","doi-asserted-by":"publisher","first-page":"4205","DOI":"10.1007\/s10664-020-09872-1","volume":"25","author":"A Iung","year":"2020","unstructured":"Iung A et al (2020) Systematic mapping study on domain-specific language development tools. Empir Softw Eng 25:4205\u20134249","journal-title":"Empir Softw Eng"},{"key":"602_CR31","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1595453.1595457","volume":"41","author":"S Liu","year":"2009","unstructured":"Liu S, Takahashi K, Hayashi T, Nakayama T (2009) Teaching formal methods in the context of software engineering. ACM SIGCSE Bulletin 41:17\u201323","journal-title":"ACM SIGCSE Bulletin"},{"key":"602_CR32","doi-asserted-by":"crossref","unstructured":"Hazel D, Strooper P, Traynor O (1997) Possum: an animator for the sum specification language. In Proceedings of Joint 4th international computer science conference and 4th Asia Pacific software engineering conference, 42\u201351","DOI":"10.1109\/APSEC.1997.640160"},{"key":"602_CR33","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1145\/990010.990012","volume":"12","author":"T Miller","year":"2003","unstructured":"Miller T, Strooper P (2003) A framework and tool support for the systematic testing of model-based specifications. ACM Trans Softw Eng Methodol 12:409\u2013439. https:\/\/doi.org\/10.1145\/990010.990012","journal-title":"ACM Trans Softw Eng Methodol"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-025-00602-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-025-00602-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-025-00602-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,6]],"date-time":"2025-09-06T17:27:33Z","timestamp":1757179653000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-025-00602-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,3]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["602"],"URL":"https:\/\/doi.org\/10.1007\/s11334-025-00602-8","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2025,6,3]]},"assertion":[{"value":"10 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}