{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,12]],"date-time":"2025-05-12T11:27:07Z","timestamp":1747049227424,"version":"3.37.3"},"reference-count":73,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T00:00:00Z","timestamp":1708387200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T00:00:00Z","timestamp":1708387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003484","name":"Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003484","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Especially in industrial applications of formal modeling, validation is as important as verification. Thus, it is important to integrate the stakeholders\u2019 and the domain experts\u2019 feedback as early as possible. In this work, we propose two approaches to enable this: (1) a static export of an animation trace into a single HTML file, and (2) a dynamic export of a classical B model as an interactive HTML document, both based on domain-specific visualizations. For the second approach, we extend the high-level code generator <jats:sc>B2Program<\/jats:sc> by JavaScript and integrate <jats:sc>VisB<\/jats:sc> visualizations alongside <jats:sc>SimB<\/jats:sc> simulations with timing, probabilistic and interactive elements. An important aspect of this work is to ease communication between modelers and domain experts. This is achieved by implementing features to run simulations, sharing animated traces with descriptions and giving feedback to each other. This work also evaluates the performance of the generated JavaScript code compared with existing approaches with Java and C++ code generation as well as the animator, constraint solver, and model checker <jats:sc>ProB<\/jats:sc>.<\/jats:p>","DOI":"10.1007\/s10009-024-00739-0","type":"journal-article","created":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T14:02:45Z","timestamp":1708437765000},"page":"147-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Generating interactive documents for domain-specific validation of formal models"],"prefix":"10.1007","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2556-5553","authenticated-orcid":false,"given":"Fabian","family":"Vu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher","family":"Happe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,2,20]]},"reference":[{"key":"739_CR1","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)"},{"key":"739_CR2","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"2005","unstructured":"Abrial, J.R., Hoare, A.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"739_CR3","unstructured":"Bagwell, P.: Ideal hash trees. Es Grands Champs 1195 (2001)"},{"key":"739_CR4","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":"739_CR5","series-title":"LNCS","first-page":"193","volume-title":"Proceedings FMICS","author":"J. Bendisposto","year":"2021","unstructured":"Bendisposto, J., Gele\u00dfus, D., Jansing, Y., Leuschel, M., P\u00fctz, A., Vu, F., Werth, M.: ProB2-UI: a Java-based user interface for ProB. In: Proceedings FMICS. LNCS, vol.\u00a012863, pp.\u00a0193\u2013201 (2021)"},{"key":"739_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Hybrid Systems III. LNCS, vol.\u00a01066, pp.\u00a0232\u2013243 (1996)"},{"key":"739_CR7","series-title":"LNCS","first-page":"295","volume-title":"Proceedings NFM","author":"S. Bonfanti","year":"2017","unstructured":"Bonfanti, S., Carissoni, M., Gargantini, A., Mashkoor, A.: Asm2C++: a tool for code generation from abstract state machines to Arduino. In: Proceedings NFM. LNCS, vol.\u00a010227, pp.\u00a0295\u2013301 (2017)"},{"key":"739_CR8","doi-asserted-by":"crossref","unstructured":"Bonfanti, S., Gargantini, A., Mashkoor, A.: Design and validation of a C++ code generator from Abstract State Machines specifications. J. Softw. Evol. Process 32 (2020)","DOI":"10.1002\/smr.2205"},{"key":"739_CR9","series-title":"LNCS","first-page":"1","volume-title":"Proceedings SBMF","author":"R. Bonichon","year":"2014","unstructured":"Bonichon, R., D\u00e9harbe, D., Lecomte, T., Medeiros, V. Jr: LLVM-based code generation for B. In: Proceedings SBMF. LNCS, vol.\u00a08941, pp.\u00a01\u201316 (2014)"},{"key":"739_CR10","series-title":"CCIS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07512-9_1","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"F. Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: ABZ 2014: The Landing Gear Case Study. CCIS, vol.\u00a0433, pp.\u00a01\u201318 (2014)"},{"key":"739_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11526841_16","volume-title":"Proceedings of Formal Methods 2005","author":"M. Butler","year":"2005","unstructured":"Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Proceedings of Formal Methods 2005. LNCS, vol.\u00a03582, pp.\u00a0221\u2013236. Springer, Newcastle upon Tyne (2005)"},{"key":"739_CR12","series-title":"LNCS","first-page":"71","volume-title":"Proceedings ABZ","author":"A. Carioni","year":"2008","unstructured":"Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A\u00a0scenario-based validation language for ASMs. In: Proceedings ABZ. LNCS, vol.\u00a05238, pp.\u00a071\u201384 (2008)"},{"key":"739_CR13","unstructured":"Carlsson, M., Widen, J., Andersson, J., Andersson, S., Boortz, K., Nilsson, H., Sj\u00f6land, T.: SICStus Prolog user\u2019s manual. Swedish Institute of Computer Science Kista, (1988)"},{"key":"739_CR14","series-title":"LNCS","first-page":"166","volume-title":"Proceedings NFM","author":"N. Cata\u00f1o","year":"2016","unstructured":"Cata\u00f1o, N., Rivera, V.: EventB2Java: a code generator for Event-B. In: Proceedings NFM. LNCS, vol.\u00a09690, pp.\u00a0166\u2013171 (2016)"},{"key":"739_CR15","unstructured":"ClearSy: User and reference manuals. Aix-en-Provence, France (2016). http:\/\/www.atelierb.eu\/"},{"issue":"1","key":"739_CR16","first-page":"11","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. Inform. 22(1), 11\u201332 (2003)","journal-title":"Tech. Sci. Inform."},{"key":"739_CR17","unstructured":"D\u00f6ring, L.: Feasibility and uses of a superset of B0 for embedded code-generation. Master\u2019s thesis, Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2023)"},{"key":"739_CR18","series-title":"LNCS","first-page":"284","volume-title":"Proceedings ABZ","author":"A. Edmunds","year":"2014","unstructured":"Edmunds, A.: Templates for Event-B code generation. In: Proceedings ABZ. LNCS, vol.\u00a08477, pp.\u00a0284\u2013289 (2014)"},{"key":"739_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11955757_21","volume-title":"B 2007: Formal Specification and Development in B","author":"D. Essam\u00e9","year":"2006","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large-scale projects: the canarsie line CBTC experience. In: B 2007: Formal Specification and Development in B. LNCS, vol.\u00a04355, pp.\u00a0252\u2013254 (2006)"},{"key":"739_CR20","series-title":"LNCS","first-page":"420","volume-title":"Proceedings NFM","author":"A.W. Fifarek","year":"2017","unstructured":"Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: Proceedings NFM. LNCS, vol.\u00a010227, pp.\u00a0420\u2013426 (2017)"},{"key":"739_CR21","series-title":"LNCS","first-page":"159","volume-title":"Proceedings RSSRail","author":"T. Fischer","year":"2019","unstructured":"Fischer, T., Dghyam, D.: Formal model validation through acceptance tests. In: Proceedings RSSRail. LNCS, vol.\u00a011495, pp.\u00a0159\u2013169 (2019)"},{"key":"739_CR22","series-title":"LNCS","first-page":"323","volume-title":"Proceedings iFM","author":"A. F\u00fcrst","year":"2014","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D.A., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Proceedings iFM. LNCS, vol.\u00a08739, pp.\u00a0323\u2013338 (2014)"},{"key":"739_CR23","series-title":"LNCS","first-page":"68","volume-title":"Proceedings TACAS","author":"H.O. Garavel","year":"1998","unstructured":"Garavel, H.O.: An open software architecture for verification, simulation, and testing. In: Proceedings TACAS. LNCS, vol.\u00a01384, pp.\u00a068\u201384 (1998)"},{"key":"739_CR24","volume-title":"Proceedings ASM Workshop","author":"A. Gargantini","year":"2007","unstructured":"Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based simulator for ASMs. In: Proceedings ASM Workshop (2007)"},{"issue":"12","key":"739_CR25","doi-asserted-by":"publisher","first-page":"1949","DOI":"10.3217\/jucs-014-12-1949","volume":"14","author":"A. Gargantini","year":"2008","unstructured":"Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J.\u00a0Univers. Comput. Sci. 14(12), 1949\u20131983 (2008). https:\/\/doi.org\/10.3217\/jucs-014-12-1949","journal-title":"J.\u00a0Univers. Comput. Sci."},{"key":"739_CR26","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1109\/ICSEA.2008.62","volume-title":"Proceedings ICSEA","author":"A. Gargantini","year":"2008","unstructured":"Gargantini, A., Riccobene, E., Scandurra, P.: Model-driven language engineering: the ASMETA case study. In: Proceedings ICSEA, pp.\u00a0373\u2013378 (2008). https:\/\/doi.org\/10.1109\/ICSEA.2008.62"},{"key":"739_CR27","series-title":"LNCS","first-page":"248","volume-title":"Proceedings ABZ","author":"D. Gele\u00dfus","year":"2020","unstructured":"Gele\u00dfus, D., Leuschel, M.: ProB and Jupyter for logic, set theory, theoretical computer science and formal methods. In: Proceedings ABZ. LNCS, vol.\u00a012071, pp.\u00a0248\u2013254 (2020)"},{"key":"739_CR28","series-title":"LNCS","first-page":"284","volume-title":"Proceedings ABZ","author":"D. Gele\u00dfus","year":"2023","unstructured":"Gele\u00dfus, D., Stock, S., Vu, F., Leuschel, M., Mashkoor, A.: Modeling and analysis of a safety-critical interactive system through validation obligations. In: Proceedings ABZ. LNCS, vol.\u00a014010, pp.\u00a0284\u2013302 (2023)"},{"key":"739_CR29","series-title":"LNCS","first-page":"19","volume-title":"Proceedings REFSQ","author":"D. Giannakopoulou","year":"2020","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Generation of formal requirements from structured natural language. In: Proceedings REFSQ. LNCS, vol.\u00a012045, pp.\u00a019\u201335 (2020)"},{"key":"739_CR30","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590","volume":"137","author":"D. Giannakopoulou","year":"2021","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Automated formalization of structured natural language requirements. Inf. Softw. Technol. 137, 106590 (2021). https:\/\/doi.org\/10.1016\/j.infsof.2021.106590","journal-title":"Inf. Softw. Technol."},{"key":"739_CR31","series-title":"LNCS","first-page":"24","volume-title":"Proceedings iFM","author":"D. Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: Proceedings iFM. LNCS, vol.\u00a07321, pp.\u00a024\u201338 (2012)"},{"key":"739_CR32","series-title":"LNCS","first-page":"40","volume-title":"Proceedings ABZ","author":"D. Hansen","year":"2014","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA+ for validation with TLC. In: Proceedings ABZ. LNCS, vol.\u00a08477, pp.\u00a040\u201355 (2014)"},{"issue":"3","key":"739_CR33","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."},{"key":"739_CR34","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley, Reading (2011)","edition":"1"},{"key":"739_CR35","series-title":"LNCS","first-page":"281","volume-title":"Proceedings ABZ","author":"F. Houdek","year":"2020","unstructured":"Houdek, F., Raschke, A.: Adaptive exterior light and speed control system. In: Proceedings ABZ. LNCS, vol.\u00a012071, pp.\u00a0281\u2013301 (2020)"},{"key":"739_CR36","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.1991.106963","volume-title":"IEEE Standard Computer Dictionary: A Compilation of IEEE Standard Computer Glossaries","author":"Institute of Electrical and Electro","year":"1991","unstructured":"Institute of Electrical and Electronics Engineers: IEEE Standard Computer Dictionary: A Compilation of IEEE Standard Computer Glossaries. IEEE, New York (1991). https:\/\/doi.org\/10.1109\/IEEESTD.1991.106963"},{"key":"739_CR37","volume-title":"Proceedings of the 12th Overture Workshop","author":"P.W.V. J\u00f8rgensen","year":"2015","unstructured":"J\u00f8rgensen, P.W.V., Larsen, M., Couto, L.D.: A code generation platform for VDM. In: Proceedings of the 12th Overture Workshop. School of Computing Science, Newcastle University, Technical Report CS-TR-1446, UK (2015)"},{"key":"739_CR38","series-title":"LNCS","first-page":"692","volume-title":"Proceedings TACAS","author":"G. Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Proceedings TACAS. LNCS, vol.\u00a09035, pp.\u00a0692\u2013707 (2015)"},{"issue":"1","key":"739_CR39","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/s10703-020-00351-3","volume":"58","author":"P. K\u00f6rner","year":"2021","unstructured":"K\u00f6rner, P., Bendisposto, J., Dunkelau, J., Krings, S., Leuschel, M.: Integrating formal specifications into applications: the ProB Java API. Form. Methods Syst. Des. 58(1), 160\u2013187 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00351-3","journal-title":"Form. Methods Syst. Des."},{"key":"739_CR40","series-title":"LNCS","first-page":"71","volume-title":"Proceedings ABZ","author":"S. Krings","year":"2018","unstructured":"Krings, S., Schmidt, J., Brings, C., Frappier, M., Leuschel, M.: A translation from Alloy to B. In: Proceedings ABZ. LNCS, vol.\u00a010817, pp.\u00a071\u201386 (2018)"},{"key":"739_CR41","unstructured":"Ladenberger, L.: Rapid creation of interactive formal prototypes for validating safety-critical systems. Ph.D. thesis, Universit\u00e4ts-und Landesbibliothek der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2016)"},{"key":"739_CR42","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-25423-4_10","volume-title":"Proceedings ICFEM","author":"L. Ladenberger","year":"2015","unstructured":"Ladenberger, L., Leuschel, M.: Mastering the visualization of larger state spaces with projection diagrams. In: Proceedings ICFEM. LNCS, vol.\u00a09407, pp.\u00a0153\u2013169 (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_10"},{"key":"739_CR43","series-title":"LNCS","first-page":"202","volume-title":"Proceedings FMICS","author":"L. Ladenberger","year":"2009","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Proceedings FMICS. LNCS, vol.\u00a05825, pp.\u00a0202\u2013204 (2009)"},{"issue":"2","key":"739_CR44","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s10009-015-0395-9","volume":"19","author":"L. Ladenberger","year":"2017","unstructured":"Ladenberger, L., Hansen, D., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. Int. J. Softw. Tools Technol. Transf. 19(2), 187\u2013203 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0395-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"739_CR45","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1668862.1668864","volume":"35","author":"P. Larsen","year":"2010","unstructured":"Larsen, P., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative: integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35, 1\u20136 (2010). https:\/\/doi.org\/10.1145\/1668862.1668864","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"739_CR46","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-49815-7_1","volume-title":"Proceedings SBMF","author":"M. Leuschel","year":"2016","unstructured":"Leuschel, M.: Formal model-based constraint solving and document generation. In: Proceedings SBMF. LNCS, vol.\u00a010090, pp.\u00a03\u201320 (2016). https:\/\/doi.org\/10.1007\/978-3-319-49815-7_1"},{"key":"739_CR47","series-title":"LNCS","first-page":"129","volume-title":"Proceedings iFM","author":"M. Leuschel","year":"2022","unstructured":"Leuschel, M.: Operation caching and state compression for model checking of high-level models \u2014 how to have your cake and eat it. In: Proceedings iFM. LNCS, vol.\u00a013274, pp.\u00a0129\u2013145 (2022)"},{"key":"739_CR48","series-title":"LNCS","first-page":"855","volume-title":"Proceedings FME","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Proceedings FME. LNCS, vol.\u00a02805, pp.\u00a0855\u2013874 (2003)"},{"issue":"2","key":"739_CR49","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.: 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":"739_CR50","first-page":"17","volume-title":"The B Method: From Research to Teaching","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Samia, M., Bendisposto, J.: Easy graphical animation and formula visualisation for teaching B. In: The B Method: From Research to Teaching, pp.\u00a017\u201332 (2008)"},{"key":"739_CR51","volume-title":"Proceedings Rodin Workshop","author":"M. Leuschel","year":"2014","unstructured":"Leuschel, M., Bendisposto, J., Hansen, D.: Unlocking the mysteries of a formal model of an interlocking system. In: Proceedings Rodin Workshop (2014)"},{"key":"739_CR52","series-title":"LNCS","first-page":"335","volume-title":"Proceedings ABZ","author":"M. Leuschel","year":"2020","unstructured":"Leuschel, M., Mutz, M., Werth, M.: Modelling and validating an automotive system in classical B and Event-B. In: Proceedings ABZ. LNCS, vol.\u00a012071, pp.\u00a0335\u2013350 (2020)"},{"issue":"3","key":"739_CR53","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s10270-016-0514-4","volume":"16","author":"A. Mashkoor","year":"2017","unstructured":"Mashkoor, A., Yang, F., Jacquot, J.: Refinement-based validation of Event-B specifications. Softw. Syst. Model. 16(3), 789\u2013808 (2017). https:\/\/doi.org\/10.1007\/s10270-016-0514-4","journal-title":"Softw. Syst. Model."},{"key":"739_CR54","first-page":"179","volume-title":"Proceedings SoICT","author":"D. M\u00e9ry","year":"2011","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings SoICT, pp.\u00a0179\u2013188. ACM ICPS (2011)"},{"key":"739_CR55","first-page":"18","volume-title":"Proceedings Overture Workshop","author":"T. Oda","year":"2015","unstructured":"Oda, T., Yamamoto, Y., Nakakoji, K., Araki, K., Larsen, P.: VDM animation for a wider range of stakeholders. In: Proceedings Overture Workshop, pp.\u00a018\u201332 (2015)"},{"key":"739_CR56","first-page":"5","volume-title":"Proceedings International Overture Workshop","author":"T. Oda","year":"2021","unstructured":"Oda, T., Akari, K., Yamamoto, Y., Nakakoji, K., Chang, H.M., Larsen, P.: Specifying abstract user interface in VDM-SL. In: Proceedings International Overture Workshop, pp.\u00a05\u201320 (2021)"},{"key":"739_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11955757_20","volume-title":"Proceedings B \u201907","author":"I. Oliver","year":"2007","unstructured":"Oliver, I.: Experiences in using B and UML in industrial development. In: Proceedings B \u201907. LNCS, vol.\u00a04355, pp.\u00a0248\u2013251 (2007). https:\/\/doi.org\/10.1007\/11955757_20"},{"key":"739_CR58","unstructured":"Parr, T.: StringTemplate website (2013). http:\/\/www.stringtemplate.org\/. Accessed: 2022-07-05"},{"issue":"1","key":"739_CR59","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10009-015-0381-2","volume":"19","author":"V. Rivera","year":"2017","unstructured":"Rivera, V., Cata\u00f1o, N., Wahls, T., Rueda, C.: Code generation for Event-B. Int. J. Softw. Tools Technol. Transf. 19(1), 31\u201352 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"739_CR60","series-title":"LNCS","first-page":"274","volume-title":"Proceedings B \u201907","author":"T. Servat","year":"2006","unstructured":"Servat, T.: BRAMA: a new graphic animation tool for B models. In: Proceedings B \u201907. LNCS, vol.\u00a04355, pp.\u00a0274\u2013276 (2006)"},{"key":"739_CR61","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2020.101833","volume":"112","author":"C. Snook","year":"2021","unstructured":"Snook, C., Hoang, T.S., Dghaym, D., Fathabadi, A.S., Butler, M.: Domain-specific scenarios for refinement-based methods. J. Syst. Archit. 112, 101833 (2021)","journal-title":"J. Syst. Archit."},{"key":"739_CR62","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.simpat.2018.12.005","volume":"92","author":"C. Thule","year":"2019","unstructured":"Thule, C., Lausdahl, K., Gomes, C., Meisl, G., Larsen, P.G.: Maestro: the INTO-CPS co-simulation framework. Simul. Model. Pract. Theory 92, 45\u201361 (2019). https:\/\/doi.org\/10.1016\/j.simpat.2018.12.005","journal-title":"Simul. Model. Pract. Theory"},{"key":"739_CR63","first-page":"137","volume-title":"Proceedings PPPJ \u201902\/IRE \u201902","author":"J.C. Voisinet","year":"2002","unstructured":"Voisinet, J.C.: JBTools: an experimental platform for the formal B method. In: Proceedings PPPJ \u201902\/IRE \u201902, pp.\u00a0137\u2013139 (2002)"},{"key":"739_CR64","series-title":"LNCS","first-page":"59","volume-title":"Proceedings ABZ","author":"F. Vu","year":"2023","unstructured":"Vu, F., Leuschel, M.: Validation of formal models by interactive simulation. In: Proceedings ABZ. LNCS, vol.\u00a014010, pp.\u00a059\u201369 (2023)"},{"key":"739_CR65","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-030-34968-4_25","volume-title":"Proceedings iFM","author":"F. Vu","year":"2019","unstructured":"Vu, F., Hansen, D., K\u00f6rner, P., Leuschel, M.: A multi-target code generator for high-level B. In: Proceedings iFM. LNCS, vol.\u00a011918, pp.\u00a0456\u2013473 (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_25"},{"key":"739_CR66","series-title":"LNCS","first-page":"81","volume-title":"Proceedings ABZ","author":"F. Vu","year":"2021","unstructured":"Vu, F., Leuschel, M., Mashkoor, A.: Validation of formal models by timed probabilistic simulation. In: Proceedings ABZ. LNCS, vol.\u00a012709, pp.\u00a081\u201396 (2021)"},{"key":"739_CR67","series-title":"LNCS","first-page":"334","volume-title":"Proceedings ICFEM","author":"F. Vu","year":"2022","unstructured":"Vu, F., Brandt, D., Leuschel, M.: Model checking B models via high-level code generation. In: Proceedings ICFEM. LNCS, vol.\u00a013478, pp.\u00a0334\u2013351 (2022)"},{"key":"739_CR68","series-title":"LNCS","first-page":"32","volume-title":"Proceedings FMICS","author":"F. Vu","year":"2022","unstructured":"Vu, F., Happe, C., Leuschel, M.: Generating domain-specific interactive validation documents. In: Proceedings FMICS. LNCS, vol.\u00a013487, pp.\u00a032\u201349 (2022)"},{"key":"739_CR69","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-322-91603-7_9","volume-title":"The MVC Design Pattern","author":"J.S. Warford","year":"2002","unstructured":"Warford, J.S.: The MVC Design Pattern, pp.\u00a0175\u2013199. Vieweg+Teubner Verlag, Wiesbaden (2002). https:\/\/doi.org\/10.1007\/978-3-322-91603-7_9"},{"key":"739_CR70","doi-asserted-by":"publisher","first-page":"95","DOI":"10.4204\/EPTCS.284.8","volume-title":"Proceedings F-IDE, EPTCS","author":"N. Watson","year":"2018","unstructured":"Watson, N., Reeves, S., Masci, P.: Integrating user design and formal models within PVSio-web. In: Proceedings F-IDE, EPTCS, vol.\u00a0284, pp.\u00a095\u2013104 (2018). https:\/\/doi.org\/10.4204\/EPTCS.284.8"},{"key":"739_CR71","series-title":"LNCS","first-page":"260","volume-title":"Proceedings ABZ","author":"M. Werth","year":"2020","unstructured":"Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Proceedings ABZ. LNCS, vol.\u00a012071, pp.\u00a0260\u2013265 (2020)"},{"key":"739_CR72","unstructured":"Witulski, J.: A Python B implementation \u2014 PyB A second tool-chain. Ph.D. thesis, Universit\u00e4ts-und Landesbibliothek der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2018)"},{"key":"739_CR73","series-title":"LNCS","first-page":"54","volume-title":"Proceedings CHARME","author":"Y. Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Proceedings CHARME. LNCS, vol.\u00a01703, pp.\u00a054\u201366 (1999)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00739-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00739-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00739-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,21]],"date-time":"2024-03-21T16:06:02Z","timestamp":1711037162000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00739-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,20]]},"references-count":73,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["739"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00739-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2024,2,20]]},"assertion":[{"value":"6 February 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}