{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T17:02:16Z","timestamp":1761930136772,"version":"3.37.3"},"reference-count":94,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T00:00:00Z","timestamp":1603238400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T00:00:00Z","timestamp":1603238400000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the <jats:sc>ProB<\/jats:sc> animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.\n<\/jats:p>","DOI":"10.1007\/s10703-020-00351-3","type":"journal-article","created":{"date-parts":[[2020,10,20]],"date-time":"2020-10-20T23:03:55Z","timestamp":1603235035000},"page":"160-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Integrating formal specifications into applications: the ProB Java API"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5914-1092","authenticated-orcid":false,"given":"Jens","family":"Bendisposto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-5554","authenticated-orcid":false,"given":"Jannik","family":"Dunkelau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-9798","authenticated-orcid":false,"given":"Sebastian","family":"Krings","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":[[2020,10,21]]},"reference":[{"key":"351_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge"},{"key":"351_CR2","doi-asserted-by":"crossref","unstructured":"Abrial JR (2006) Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th international conference on software engineering, pp 761\u2013768","DOI":"10.1145\/1134285.1134406"},{"key":"351_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: system and software engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial JR (2010) Modeling in Event-B: system and software engineering, 1st edn. Cambridge University Press, Cambridge","edition":"1"},{"key":"351_CR4","doi-asserted-by":"crossref","unstructured":"Abrial JR, Lee MK, Neilson D, Scharbach P, S\u00f8rensen IH (1991) The B-method. In: Proceedings VDM, LNCS, vol 552. Springer, pp 398\u2013405","DOI":"10.1007\/BFb0020001"},{"issue":"1","key":"351_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"R Back","year":"1981","unstructured":"Back R (1981) On correct refinement of programs. J Comput Syst Sci 23(1):49\u201368","journal-title":"J Comput Syst Sci"},{"key":"351_CR6","volume-title":"Refinement calculus: a systematic introduction","author":"RJ Back","year":"2012","unstructured":"Back RJ, Wright J (2012) Refinement calculus: a systematic introduction. Springer, Berlin"},{"key":"351_CR7","unstructured":"Bandur V, Tran-J\u00f8rgensen PW, Hasanagic M, Lausdahl K (2017) Code-generating VDM for embedded devices. In: Proceedings of the 15th overture workshop, School of Computing Science technical report series, vol 1513. School of Computing Science, University of Newcastle upon Tyne, pp 1\u201315"},{"issue":"11","key":"351_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y et al (2003) Bounded model checking. Adv Comput 58(11):117\u2013148","journal-title":"Adv Comput"},{"key":"351_CR9","doi-asserted-by":"crossref","unstructured":"Blochwitz T, Otter M, Akesson J, Arnold M, Clauss C, Elmqvist H, Friedrich M, Junghanns A, Mauss J, Neumerkel D et\u00a0al (2012) Functional mockup interface 2.0: the standard for tool independent exchange of simulation models. In: Proceedings MODELICA, 076. Link\u00f6ping University Electronic Press, pp 173\u2013184","DOI":"10.3384\/ecp12076173"},{"key":"351_CR10","doi-asserted-by":"crossref","unstructured":"Bonichon R, D\u00e9harbe D, Lecomte T, Medeiros V (2014) LLVM-based code generation for B. In: Proceedings SBMF, LNCS, vol 8941. Springer, pp 1\u201316","DOI":"10.1007\/978-3-319-15075-8_1"},{"key":"351_CR11","doi-asserted-by":"crossref","unstructured":"Butler M, Leuschel M (2005) Combining CSP and B for specification and property verification. In: Proceedings FM, LNCS, vol. 3582. Springer, pp 221\u2013236","DOI":"10.1007\/11526841_16"},{"key":"351_CR12","doi-asserted-by":"crossref","unstructured":"Butler MJ, Colley J, Edmunds A, Snook CF, Evans N, Grant N, Marshall H (2013) Modelling and refinement in CODA. In: Proceedings refine, vol 115. Open Publishing Association, pp 36\u201351","DOI":"10.4204\/EPTCS.115.3"},{"issue":"3\u20134","key":"351_CR13","first-page":"221","volume":"22","author":"D Cansell","year":"2012","unstructured":"Cansell D, M\u00e9ry D (2012) Foundations of the B method. Comput Inform 22(3\u20134):221\u2013256","journal-title":"Comput Inform"},{"key":"351_CR14","doi-asserted-by":"crossref","unstructured":"Cansell D, M\u00e9ry D, Rehm J (2007) Time constraint patterns for event B development. In: Proceedings B, LNCS, vol 4355. Springer, pp 140\u2013154","DOI":"10.1007\/11955757_13"},{"key":"351_CR15","doi-asserted-by":"crossref","unstructured":"Carlsson M, Ottosson G, Carlson B (1997) An open-ended finite domain constraint solver. In: Proceedings PLILP, LNCS, vol 1292. Springer, pp 191\u2013206","DOI":"10.1007\/BFb0033845"},{"key":"351_CR16","volume-title":"SICStus prolog user\u2019s manual","author":"M Carlsson","year":"1988","unstructured":"Carlsson M, Widen J, Andersson J, Andersson S, Boortz K, Nilsson H, Sj\u00f6land T (1988) SICStus prolog user\u2019s manual, vol 3. Swedish Institute of Computer Science, Kista"},{"key":"351_CR17","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o N, Rivera V (2016) EventB2Java: a code generator for event-B. In: Proceedings NFM, LNCS, vol 9690. Springer, pp 166\u2013171","DOI":"10.1007\/978-3-319-40648-0_13"},{"key":"351_CR18","unstructured":"CENELEC: railway applications\u2014communication, signalling and processing systems\u2014software for railway control and protection systems. Tech. Rep. EN50128, European Standard (2011)"},{"key":"351_CR19","doi-asserted-by":"crossref","unstructured":"Clark J, Bendisposto J, Hallerstede S, Hanse D, Leuschel M (2016) Generating event-B specifications from algorithm descriptions. In: Proceedings ABZ, LNCS, vol 9675. Springer, pp 183\u2013197","DOI":"10.1007\/978-3-319-33600-8_11"},{"key":"351_CR20","unstructured":"ClearSy: Atelier B, user and reference manuals. Aix-en-Provence, France (2016). http:\/\/www.atelierb.eu\/"},{"key":"351_CR21","doi-asserted-by":"crossref","unstructured":"Comptier M, Leuschel M, Mejia L, Perez JM, Mutz M (2019) Property-based modelling and validation of a CBTC zone controller in Event-B. In: Proceedings RSSRail, LNCS, vol 11495. Springer, pp 202\u2013212","DOI":"10.1007\/978-3-030-18744-6_13"},{"key":"351_CR22","doi-asserted-by":"crossref","unstructured":"de\u00a0Azevedo\u00a0Oliveira D, Medeiros V, D\u00e9harbe D, Musicante MA (2019) BTestBox: a tool for testing B translators and coverage of B models. In: Proceedings TAP, LNCS, vol 11823. Springer, pp 83\u201392","DOI":"10.1007\/978-3-030-31157-5_6"},{"key":"351_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proceedings TACAS, LNCS, vol 4963. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"1\u20132","key":"351_CR24","first-page":"71","volume":"77","author":"R Farahbod","year":"2007","unstructured":"Farahbod R, Gervasi V, Gl\u00e4sser U (2007) CoreASM: an extensible ASM execution engine. Fundamenta Informaticae 77(1\u20132):71\u2013103","journal-title":"Fundamenta Informaticae"},{"key":"351_CR25","doi-asserted-by":"crossref","unstructured":"Fathy HK, Filipi ZS, Hagena J, Stein JL (2006) Review of hardware-in-the-loop simulation and its prospects in the automotive area. In: Modeling and simulation for military applications, vol 6228. SPIE","DOI":"10.1117\/12.667794"},{"key":"351_CR26","doi-asserted-by":"crossref","unstructured":"Fischer T, Dghaym D (2019) Formal model validation through acceptance tests. In: Proceedings RSSRail, LNCS, vol 11495. Springer, pp 159\u2013169","DOI":"10.1007\/978-3-030-18744-6_10"},{"key":"351_CR27","doi-asserted-by":"crossref","unstructured":"Fitzgerald J, Larsen PG, Pierce K (2019) Multi-modelling and co-simulation in the engineering of cyber-physical systems: towards the digital twin. In: From software engineering to formal methods and tools, and back, LNCS, vol 11865. Springer, pp 40\u201355","DOI":"10.1007\/978-3-030-30985-5_4"},{"issue":"3","key":"351_CR28","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/BF01457986","volume":"86","author":"A Fraenkel","year":"1922","unstructured":"Fraenkel A (1922) Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre. Mathematische Annalen 86(3):230\u2013237","journal-title":"Mathematische Annalen"},{"key":"351_CR29","volume-title":"Foundations of set theory","author":"AA Fraenkel","year":"1973","unstructured":"Fraenkel AA, Bar-Hillel Y, Levy A (1973) Foundations of set theory, vol 67. Elsevier, Amsterdam"},{"issue":"5","key":"351_CR30","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1049\/sej.1992.0033","volume":"7","author":"NE Fuchs","year":"1992","unstructured":"Fuchs NE (1992) Specifications are (preferably) executable. Softw Eng J 7(5):323\u2013334","journal-title":"Softw Eng J"},{"key":"351_CR31","doi-asserted-by":"crossref","unstructured":"Gelessus D, Leuschel M (2020) ProB and Jupyter for logic, set theory, theoretical computer science and formal methods. In: Proceedings ABZ 2020, LNCS, vol 12071. Springer, pp 248\u2013254 (2020)","DOI":"10.1007\/978-3-030-48077-6_19"},{"key":"351_CR32","doi-asserted-by":"crossref","unstructured":"Ghezzi C, Kennerer RA (1991) Executing formal specifications: the ASTRAL to TRIO translation approach. In: Proceedings TAV. ACM, pp 112\u2013122","DOI":"10.1145\/120807.120817"},{"key":"351_CR33","doi-asserted-by":"crossref","unstructured":"Gomes C, Thule C, Broman D, Larsen PG, Vangheluwe H (2017) Co-simulation: state of the art. arXiv:1702.00686v1","DOI":"10.1145\/3179993"},{"key":"351_CR34","unstructured":"Google Guice Repository. https:\/\/github.com\/google\/guice. Accessed 27 Feb 2020"},{"issue":"2","key":"351_CR35","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1049\/sej.1996.0014","volume":"11","author":"A Gravell","year":"1996","unstructured":"Gravell A, Henderson P (1996) Executing formal specifications need not be harmful. Softw Eng J 11(2):104\u2013110","journal-title":"Softw Eng J"},{"key":"351_CR36","doi-asserted-by":"crossref","unstructured":"Grov G, Ireland A, Llano MT (2012) Refinement plans for informed formal design. In: Proceedings ABZ, LNCS, vol 7316. Springer, pp 208\u2013222","DOI":"10.1007\/978-3-642-30885-7_15"},{"key":"351_CR37","doi-asserted-by":"crossref","unstructured":"Hansen D, Leuschel M (2012) Translating TLA+ to B for validation with ProB. In: Proceedings IFM, LNCS, vol 7321. Springer, pp 24\u201338","DOI":"10.1007\/978-3-642-30729-4_3"},{"key":"351_CR38","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 (2020) Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model. STTT 22:315\u2013332","journal-title":"STTT"},{"key":"351_CR39","doi-asserted-by":"crossref","unstructured":"Hansen D, Leuschel M, Schneider D, Krings S, K\u00f6rner P, Naulin T, Nayeri N, Skowron F (2018) Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains. In: Proceedings ABZ, LNCS, vol 10817. Springer, pp 292\u2013306","DOI":"10.1007\/978-3-319-91271-4_20"},{"key":"351_CR40","doi-asserted-by":"crossref","unstructured":"Harel D, Marron A, Rosenfeld A, Vardi M, Weiss G (2019) Labor division with movable walls: composing executable specifications with machine learning and search (Blue Sky Idea). In: Proceedings AAAI, vol\u00a033. Association for the Advancement of Artificial Intelligence, pp 9770\u20139774","DOI":"10.1609\/aaai.v33i01.33019770"},{"issue":"6","key":"351_CR41","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1049\/sej.1989.0045","volume":"4","author":"IJ Hayes","year":"1989","unstructured":"Hayes IJ, Jones CB (1989) Specifications are not (necessarily) executable. Softw Eng J 4(6):330\u2013339","journal-title":"Softw Eng J"},{"key":"351_CR42","doi-asserted-by":"crossref","unstructured":"Henzinger TA (2000) The theory of hybrid automata. In: Verification of digital and hybrid systems. Springer, pp 265\u2013292","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"351_CR43","doi-asserted-by":"crossref","unstructured":"Hickey R (2020) A history of Clojure. In: Proceedings of the ACM on programming languages, vol 4 (HOPL), pp 1\u201346","DOI":"10.1145\/3386321"},{"key":"351_CR44","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1978) Communicating sequential processes. In: The origin of concurrent programming. Springer, pp 413\u2013443","DOI":"10.1007\/978-1-4757-3472-0_16"},{"key":"351_CR45","doi-asserted-by":"crossref","unstructured":"Idani A, Ledru Y, Wakrime AA, Ayed RB, Bon P (2019) Towards a tool-based domain specific approach for railway systems modeling and validation. In: Proceedings RSSRail, LNCS, vol 11495. Springer, pp 23\u201340","DOI":"10.1007\/978-3-030-18744-6_2"},{"key":"351_CR46","doi-asserted-by":"crossref","unstructured":"Iliasov A, Lopatkin I, Romanovsky A (2013) The SafeCap platform for modelling railway safety and capacity. In: Proceedings SAFECOMP, LNCS, vol 8153. Springer, pp 130\u2013137","DOI":"10.1007\/978-3-642-40793-2_12"},{"key":"351_CR47","doi-asserted-by":"crossref","unstructured":"Jarvinen H, Kurki-Suonio R, Sakkinen M, Systa K (1990) Object-oriented specification of reactive systems. In: Proceedings ICSE. IEEE, pp 63\u201371","DOI":"10.1109\/ICSE.1990.63604"},{"key":"351_CR48","volume-title":"Systematic software development using VDM","author":"CB Jones","year":"1990","unstructured":"Jones CB (1990) Systematic software development using VDM, vol 2. Prentice-Hall, Upper Saddle River"},{"key":"351_CR49","unstructured":"J\u00f8rgensen PWV, Larsen M, Couto LDMD (2015) A code generation platform for VDM. In: Proceedings of the 12th overture workshop, School of Computing Science Technical report series, vol 1446. School of Computing Science, University of Newcastle upon Tyne, pp 21\u201335"},{"issue":"4","key":"351_CR50","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0004-3702(75)90019-3","volume":"6","author":"DE Knuth","year":"1975","unstructured":"Knuth DE, Moore RW (1975) An analysis of alpha-beta pruning. Artif Intell 6(4):293\u2013326","journal-title":"Artif Intell"},{"key":"351_CR51","doi-asserted-by":"crossref","unstructured":"K\u00f6rner P, Bendisposto J, Dunkelau J, Krings S, Leuschel M (2019) Embedding high-level formal specifications into applications. In: Proceedings FM, LNCS, vol 11800. Springer, pp 519\u2013535","DOI":"10.1007\/978-3-030-30942-8_31"},{"key":"351_CR52","doi-asserted-by":"crossref","unstructured":"Kupferschmid S, Hoffmann J, Dierks H, Behrmann G (2006) Adapting an AI planning heuristic for directed model checking. In: Proceedings SPIN, LNCS, vol 3925. Springer, pp 35\u201352","DOI":"10.1007\/11691617_3"},{"key":"351_CR53","unstructured":"Ladenberger L (2017) Rapid creation of interactive formal prototypes for validating safety-critical systems. Ph.D. thesis, HHU D\u00fcsseldorf"},{"key":"351_CR54","doi-asserted-by":"crossref","unstructured":"Ladenberger L, Leuschel M (2016) BMotionWeb: a tool for rapid creation of formal prototypes. In: Software engineering and formal methods, LNCS, vol 9763. Springer, pp 403\u2013417","DOI":"10.1007\/978-3-319-41591-8_27"},{"key":"351_CR55","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2002","unstructured":"Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc, Boston"},{"issue":"1","key":"351_CR56","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1668862.1668864","volume":"35","author":"PG Larsen","year":"2010","unstructured":"Larsen PG, Battle N, Ferreira M, Fitzgerald J, Lausdahl K, Verhoef M (2010) The overture initiative integrating tools for VDM. ACM SIGSOFT Softw Eng Notes 35(1):1\u20136","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"351_CR57","doi-asserted-by":"crossref","unstructured":"Larsen PG, Fitzgerald J, Woodcock J, Fritzson P, Brauer J, Kleijn C, Lecomte T, Pfeil M, Green O, Basagiannis S et al (2016) Integrated tool chain for model-based design of cyber-physical systems: the INTO-CPS project. In: Proceedings CPS Data. IEEE, pp 1\u20136","DOI":"10.1109\/CPSData.2016.7496424"},{"key":"351_CR58","unstructured":"Lausdahl K, Ishikawa H, Larsen PG (2015) Interpreting implicit VDM specifications using ProB. In: Proceedings of the 12th overture workshop, School of Computing Science Technical Report Series, vol 1446. School of Computing Science, University of Newcastle upon Tyne, pp 6\u201320"},{"key":"351_CR59","unstructured":"Lecomte T, Burdy L, Leuschel M (2012) Formally checking large data sets in the railways. arXiv:1210.6815"},{"key":"351_CR60","doi-asserted-by":"crossref","unstructured":"Leuschel M, Bendisposto J (2011) Directed model checking for B: an evaluation and new techniques. In: Proceedings SBMF, LNCS, vol 6527. Springer, pp 1\u201316","DOI":"10.1007\/978-3-642-19829-8_1"},{"key":"351_CR61","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2003) ProB: a model checker for B. In: Proceedings FME, LNCS, vol 2805. Springer, pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"351_CR62","doi-asserted-by":"crossref","unstructured":"Leuschel M, Mutz M, Werth M (2020) Modelling and validating an automotive system in classical B and event-B. In: Proceedings ABZ, LNCS, vol 12071. Springer, pp 335\u2013350","DOI":"10.1007\/978-3-030-48077-6_27"},{"key":"351_CR63","unstructured":"Logic Calculators. https:\/\/web.archive.org\/web\/20120418155039\/http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/logic-calculators.html. Accessed 27 Feb 2020"},{"key":"351_CR64","doi-asserted-by":"crossref","unstructured":"M\u00e9ry D, Singh NK (2011) Automatic code generation from event-B models. In: Proceedings SoICT. ACM, pp 179\u2013188","DOI":"10.1145\/2069216.2069252"},{"key":"351_CR65","doi-asserted-by":"crossref","unstructured":"Narayanasamy S, Pokam G, Calder B (2005) Bugnet: continuously recording program execution for deterministic replay debugging. In: ACM SIGARCH computer architecture news, vol\u00a033. IEEE Computer Society, pp 284\u2013295","DOI":"10.1145\/1080695.1069994"},{"key":"351_CR66","doi-asserted-by":"crossref","unstructured":"Nielsen CB, Lausdahl K, Larsen PG (2012) Combining VDM with executable code. In: Proceedings ABZ, LNCS, vol 7316. Springer, pp 266\u2013279","DOI":"10.1007\/978-3-642-30885-7_19"},{"key":"351_CR67","unstructured":"Nummenmaa T (2013) Executable formal specifications in game development: design, validation and evolution. Ph.D. thesis, University of Tampere"},{"key":"351_CR68","doi-asserted-by":"crossref","unstructured":"Plagge D, Leuschel M (2007) Validating Z specifications using the ProB animator and model checker. In: Proceedings IFM, LNCS, vol 4591. Springer, pp 480\u2013500","DOI":"10.1007\/978-3-540-73210-5_25"},{"key":"351_CR69","unstructured":"Pl\u00fcS. https:\/\/plues.github.io\/en\/index\/. Accessed 27 Feb 2020"},{"key":"351_CR70","doi-asserted-by":"crossref","unstructured":"Poulding S, Feldt R (2015) Heuristic model checking using a monte-carlo tree search algorithm. In: Proceedings GECCO. ACM, pp 1359\u20131366","DOI":"10.1145\/2739480.2754767"},{"key":"351_CR71","unstructured":"ProB Java API Source Code. https:\/\/github.com\/hhu-stups\/prob2_kernel. Accessed 11 Mar 2020"},{"key":"351_CR72","unstructured":"ProB Java API Example Source Code. https:\/\/github.com\/hhu-stups\/executable_spec_example. Accessed 11 Mar 2020"},{"key":"351_CR73","unstructured":"ProB Maven Artifacts. https:\/\/search.maven.org\/artifact\/de.hhu.stups\/de.prob2.kernel. Accessed 11 Mar 2020"},{"key":"351_CR74","unstructured":"Rehm J, Cansell D (2007) Proved development of the real-time properties of the IEEE 1394 root contention protocol with the event B method. In: Proceedings ISoLA, Revue des Nouvelles Technologies de l\u2019Information, vol RNTI-SM-1. C\u00e9padu\u00e8s-\u00c9ditions, pp 179\u2013190"},{"issue":"1","key":"351_CR75","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 (2017) Code generation for event-B. STTT 19(1):31\u201352","journal-title":"STTT"},{"key":"351_CR76","unstructured":"Rodriguez MTL (2013) Invariant discovery and refinement plans for formal modelling in Event-B. Ph.D. thesis, Heriot-Watt University, UK"},{"key":"351_CR77","unstructured":"Savary A, Lanet JL, Frappier M, Razafindralambo T, Dolhen J (2012) VTG\u2014vulnerability test generator, a plug-in for rodin. In: Workshop deploy 2012. Fontainebleau, France"},{"key":"351_CR78","doi-asserted-by":"crossref","unstructured":"Schmidt J, Krings S, Leuschel M (2018) Repair and generation of formal models using synthesis. In: Proceedings IFM, LNCS, vol 11023. Springer, pp 346\u2013366","DOI":"10.1007\/978-3-319-98938-9_20"},{"key":"351_CR79","unstructured":"Schneider D (2017) Constraint modelling and data validation using formal specification languages. Ph.D. thesis, Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf"},{"key":"351_CR80","doi-asserted-by":"crossref","unstructured":"Schneider D, Leuschel M, Witt T (2018) Model-based problem solving for university timetable validation and improvement. In: Formal aspects of computing, pp 545\u2013569","DOI":"10.1007\/s00165-018-0461-7"},{"issue":"7","key":"351_CR81","doi-asserted-by":"publisher","first-page":"1163","DOI":"10.1016\/j.jss.2007.08.026","volume":"81","author":"M Short","year":"2008","unstructured":"Short M, Pont MJ (2008) Assessment of high-integrity embedded automotive control systems using hardware in the loop simulation. J Syst Softw 81(7):1163\u20131183","journal-title":"J Syst Softw"},{"key":"351_CR82","doi-asserted-by":"crossref","unstructured":"Smaus JG, Hoffmann J (2009) Relaxation refinement: a new method to generate heuristic functions. In: Postproceedings MOCHART 2008, LNAI, vol 5348. Springer, pp 147\u2013165","DOI":"10.1007\/978-3-642-00431-5_10"},{"key":"351_CR83","volume-title":"The Z notation","author":"JM Spivey","year":"1992","unstructured":"Spivey JM, Abrial J (1992) The Z notation. Prentice Hall Hemel Hempstead, Englewood Cliffs"},{"key":"351_CR84","unstructured":"The ProB Logic Calculator. https:\/\/github.com\/hhu-stups\/prob-logic-calculator. Accessed 10 July 2020"},{"key":"351_CR85","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 PG (2019) Maestro: the INTO-CPS co-simulation framework. Simul Model Pract Theory 92:45\u201361","journal-title":"Simul Model Pract Theory"},{"key":"351_CR86","unstructured":"Thule C, Lausdahl K, Larsen PG (2018) Overture FMU: export VDM-RT models as tool-wrapper FMUs. In: Proceedings of the 16th overture workshop, School of Computing Science Technical Report Series, vol 1524. School of Computing Science, University of Newcastle upon Tyne, pp 23\u201338"},{"key":"351_CR87","unstructured":"Thule C, Nilsson R (2016) Considering abstraction levels on a case study. In: The 14th overture workshop: towards analytical tool chains, vol 4. The Electronics and Computer Engineering. Aarhus University, Department of Engineering, pp 16\u201331"},{"issue":"2","key":"351_CR88","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10009-017-0448-3","volume":"20","author":"PW Tran-J\u00f8rgensen","year":"2018","unstructured":"Tran-J\u00f8rgensen PW, Larsen PG, Leavens GT (2018) Automated translation of VDM to JML-annotated Java. STTT 20(2):211\u2013235","journal-title":"STTT"},{"key":"351_CR89","doi-asserted-by":"crossref","unstructured":"Vu F, Hansen D, K\u00f6rner P, Leuschel M (2019) A multi-target code generator for high-level B. In: Proceedings iFM, LNCS, vol 11918. Springer, pp 456\u2013473","DOI":"10.1007\/978-3-030-34968-4_25"},{"issue":"4","key":"351_CR90","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026554217992","volume":"7","author":"T Wahls","year":"2000","unstructured":"Wahls T, Leavens GT, Baker AL (2000) Executing formal specifications with concurrent constraint programming. Autom Softw Eng 7(4):315\u2013343","journal-title":"Autom Softw Eng"},{"key":"351_CR91","doi-asserted-by":"crossref","unstructured":"Watson N, Reeves S, Masci P (2018) Integrating user design and formal models within PVSio-Web. In: Proceedings F-IDE, vol 284. Open Publishing Association, pp 95\u2013104","DOI":"10.4204\/EPTCS.284.8"},{"key":"351_CR92","doi-asserted-by":"crossref","unstructured":"Werth M, Leuschel M (2020) VisB: a lightweight tool to visualize formal models with SVG graphics. In: Proceedings ABZ 2020, LNCS, vol 12071. Springer, pp 260\u2013265","DOI":"10.1007\/978-3-030-48077-6_21"},{"key":"351_CR93","first-page":"571","volume":"2013","author":"F Yang","year":"2013","unstructured":"Yang F, Jacquot J, Souqui\u00e8res J (2013) JeB: safe simulation of event-B models in javascript. Proc APSEC 2013:571\u2013576","journal-title":"Proc APSEC"},{"key":"351_CR94","doi-asserted-by":"crossref","unstructured":"Zenzaro S, Gervasi V, Soldani J (2014) WebASM: an abstract state machine execution environment for the web. In: Proceedings ABZ, LNCS, vol 8477. Springer, pp 216\u2013221","DOI":"10.1007\/978-3-662-43652-3_19"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00351-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00351-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00351-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:51:26Z","timestamp":1661529086000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00351-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,21]]},"references-count":94,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["351"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00351-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2020,10,21]]},"assertion":[{"value":"12 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 September 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with ethical standards"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}]}}