{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:41:26Z","timestamp":1779392486157,"version":"3.53.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:00:00Z","timestamp":1716768000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:00:00Z","timestamp":1716768000000},"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,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this article, we present an approach to the ABZ 2020 case study that differs from those usually presented at ABZ: Rather than using a (correct-by-construction) approach following a formal method, we use C for a low-level implementation instead. We strictly adhere to test-driven development for validation, and only afterwards apply model checking using CBMC for verification. While the approach has several benefits compared to the more rigorous approaches, it also provides less mathematical clarity and overall less thorough verification. In consequence, our realization of the ABZ case study serves as a baseline reference for comparison, allowing to assess the benefit provided by the various formal modeling languages, methods and tools.<\/jats:p>","DOI":"10.1007\/s10009-024-00750-5","type":"journal-article","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T10:01:37Z","timestamp":1716804097000},"page":"403-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A verified low-level implementation and visualization of the adaptive exterior light and speed control system"],"prefix":"10.1007","volume":"26","author":[{"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jannik","family":"Dunkelau","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kristin","family":"Rutenkolk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,27]]},"reference":[{"key":"750_CR1","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.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"750_CR2","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, New York (2010)"},{"issue":"2","key":"750_CR3","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/spe.1019","volume":"41","author":"P. Arcaini","year":"2011","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Exp. 41(2), 155\u2013166 (2011)","journal-title":"Softw. Pract. Exp."},{"key":"750_CR4","first-page":"302","volume-title":"Proceedings ABZ","author":"P. Arcaini","year":"2020","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Modelling an automotive software-intensive system with adaptive features using ASMETA. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Proceedings ABZ, pp.\u00a0302\u2013317. Springer, Cham (2020)"},{"key":"750_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-319-99725-4_2","volume-title":"Proceedings Static Analysis","author":"R. Bagnara","year":"2018","unstructured":"Bagnara, R., Bagnara, A., Hill, P.M.: The MISRA C coding standard and its role in the development and analysis of safety- and security-critical embedded software. In: Podelski, A. (ed.) Proceedings Static Analysis, pp.\u00a05\u201323. Springer, Cham (2018)"},{"key":"750_CR6","series-title":"Proceedings XP\/Agile Universe, LNCS","volume-title":"Combining Formal Specifications with Test Driven Development","author":"H. Baumeister","year":"2004","unstructured":"Baumeister, H.: Combining Formal Specifications with Test Driven Development. Proceedings XP\/Agile Universe, LNCS, vol.\u00a03134. Springer, Berlin (2004)"},{"key":"750_CR7","volume-title":"Test-Driven Development: By Example","author":"K. Beck","year":"2003","unstructured":"Beck, K.: Test-Driven Development: By Example. Kent Beck Signature Book, Addison-Wesley (2003)"},{"key":"750_CR8","first-page":"193","volume-title":"Proceedings TACAS, LNCS","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings TACAS, LNCS, vol.\u00a01579, pp.\u00a0193\u2013207. Springer, Berlin (1999)"},{"key":"750_CR9","first-page":"277","volume-title":"Proceedings ICSM","author":"C. Boogerd","year":"2008","unstructured":"Boogerd, C., Moonen, L.: Assessing the value of coding standards: an empirical study. In: Proceedings ICSM, pp.\u00a0277\u2013286. IEEE, New York (2008)"},{"key":"750_CR10","volume-title":"Proceedings ASM","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., Gargantini, A., et al.: Proceedings ASM, vol.\u00a02589. Springer, Berlin (2003)"},{"issue":"4","key":"750_CR11","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/52.391826","volume":"12","author":"J.P. Bowen","year":"1995","unstructured":"Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods. IEEE Softw. 12(4), 34\u201341 (1995)","journal-title":"IEEE Softw."},{"key":"750_CR12","first-page":"214","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods, Third International Symposium of Formal Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18\u201322, 1996, Proceedings","author":"T.M. Brookes","year":"1996","unstructured":"Brookes, T.M., Fitzgerald, J.S., Larsen, P.G.: Formal and informal specifications of a secure system component: final results in a comparative study. In: Gaudel, M., Woodcock, J. (eds.) FME \u201996: Industrial Benefit and Advances in Formal Methods, Third International Symposium of Formal Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18\u201322, 1996, Proceedings, vol.\u00a01051, pp.\u00a0214\u2013227. Springer, Berlin (1996)"},{"issue":"4","key":"750_CR13","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1109\/TSE.2009.70","volume":"36","author":"R.P. Buse","year":"2010","unstructured":"Buse, R.P., Weimer, W.R.: Learning a metric for code readability. IEEE Trans. Softw. Eng. 36(4), 546\u2013558 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"750_CR14","first-page":"209","volume-title":"Proceedings OSDI","author":"C. Cadar","year":"2008","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings OSDI, vol.\u00a08, pp.\u00a0209\u2013224. USENIX Association (2008)"},{"key":"750_CR15","first-page":"442","volume-title":"Proceedings TACAS, LNCS","author":"M. Chalupa","year":"2018","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strej\u010dek, J.: Symbiotic 5: boosted instrumentation. In: Proceedings TACAS, LNCS, vol.\u00a010806, pp.\u00a0442\u2013446. Springer, Berlin (2018)"},{"key":"750_CR16","first-page":"65","volume-title":"Proceedings UTP, LNCS","author":"M. Chen","year":"2017","unstructured":"Chen, M., Ravn, A.P., Wang, S., Yang, M., Zhan, N.: A two-way path between formal and informal design of embedded systems. In: Proceedings UTP, LNCS, vol.\u00a010134, pp.\u00a065\u201392. Springer, Berlin (2017)"},{"key":"750_CR17","first-page":"368","volume-title":"Proceedings DAC","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Proceedings DAC, pp.\u00a0368\u2013371. IEEE, New York (2003)"},{"key":"750_CR18","first-page":"168","volume-title":"Proceedings TACAS, LNCS","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proceedings TACAS, LNCS, vol.\u00a02988, pp.\u00a0168\u2013176. Springer, Berlin (2004)"},{"key":"750_CR19","volume-title":"Software Product Lines","author":"P. Clements","year":"2002","unstructured":"Clements, P., Northrop, L.: Software Product Lines. Addison-Wesley, Boston (2002)"},{"key":"750_CR20","first-page":"318","volume-title":"Proceedings ABZ","author":"A. Cunha","year":"2020","unstructured":"Cunha, A., Macedo, N., Liu, C.: Validating multiple variants of an automotive light system with electrum. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Proceedings ABZ, pp.\u00a0318\u2013334. Springer, Cham (2020)"},{"key":"750_CR21","doi-asserted-by":"publisher","DOI":"10.1117\/12.667794","volume-title":"Modeling and Simulation for Military Applications","author":"H.K. Fathy","year":"2006","unstructured":"Fathy, H.K., Filipi, Z.S., Hagena, J., Stein, J.L.: Review of hardware-in-the-loop simulation and its prospects in the automotive area. In: Modeling and Simulation for Military Applications, vol.\u00a06228. SPIE, Bellingham (2006)"},{"key":"750_CR22","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-58555-9_85","volume-title":"FME \u201994: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe","author":"J.S. Fitzgerald","year":"1994","unstructured":"Fitzgerald, J.S., Brookes, T.M., Green, M.A., Larsen, P.G.: Formal and informal specifications of a secure system component: first results in a comparative study. In: Naftalin, M., Denvir, B.T., Bertran, M. (eds.) FME \u201994: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24\u201318, 1994. Proceedings, Lecture Notes in Computer Science, vol.\u00a0873, pp.\u00a035\u201344. Springer, Berlin (1994)"},{"key":"750_CR23","unstructured":"General Specification of Basic Software Modules. AUTOSAR, Munich (2019)"},{"issue":"5","key":"750_CR24","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A. Hall","year":"1990","unstructured":"Hall, A.: Seven myths of formal methods. IEEE Softw. 7(5), 11\u201319 (1990)","journal-title":"IEEE Softw."},{"key":"750_CR25","first-page":"1","volume-title":"ABZ 2014: The Landing Gear Case Study, CCIS","author":"D. Hansen","year":"2015","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: ABZ 2014: The Landing Gear Case Study, CCIS, vol.\u00a0433, pp.\u00a01\u201317. Springer, Berlin (2015)"},{"key":"750_CR26","first-page":"292","volume-title":"Proceedings ABZ, LNCS","author":"D. Hansen","year":"2018","unstructured":"Hansen, D., Leuschel, M., Schneider, D., Krings, S., K\u00f6rner, P., Naulin, T., Nayeri, N., Skowron, F.: 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.\u00a010817, pp.\u00a0292\u2013306. Springer, Berlin (2018)"},{"issue":"5","key":"750_CR27","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.infsof.2006.07.004","volume":"49","author":"L. Hatton","year":"1998","unstructured":"Hatton, L.: Language subsetting in an industrial context: a comparison of MISRA C 1998 and MISRA C 2004. Inf. Softw. Technol. 49(5), 475\u2013482 (1998)","journal-title":"Inf. Softw. Technol."},{"key":"750_CR28","unstructured":"Houdek, F., Raschke, A.: Adaptive Exterior Light and Speed Control System"},{"key":"750_CR29","volume-title":"Road Vehicles \u2013 Functional Safety","author":"ISO","year":"2011","unstructured":"ISO: Road Vehicles \u2013 Functional Safety (2011)"},{"key":"750_CR30","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"750_CR31","first-page":"513","volume-title":"Proceedings IEEE ICSME","author":"J. Johnson","year":"2019","unstructured":"Johnson, J., Lubo, S., Yedla, N., Aponte, J., Sharif, B.: An empirical study assessing source code readability in comprehension. In: Proceedings IEEE ICSME, pp.\u00a0513\u2013523 (2019)"},{"key":"750_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-33253-4","volume-title":"Software Product Lines","author":"T. K\u00e4k\u00f6la","year":"2006","unstructured":"K\u00e4k\u00f6la, T., Duenas, J.C.: Software Product Lines. Springer, Berlin (2006)"},{"key":"750_CR33","doi-asserted-by":"crossref","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., 1\u201328 (2020)","DOI":"10.1007\/s10703-020-00351-3"},{"key":"750_CR34","first-page":"382","volume-title":"Proceedings ABZ","author":"S. Krings","year":"2020","unstructured":"Krings, S., K\u00f6rner, P., Dunkelau, J., Rutenkolk, C.: A verified low-level implementation of the adaptive exterior light and speed control system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Proceedings ABZ, pp.\u00a0382\u2013397. Springer, Cham (2020)"},{"issue":"3","key":"750_CR35","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/52.493020","volume":"13","author":"P.G. Larsen","year":"1996","unstructured":"Larsen, P.G., Fitzgerald, J.S., Brookes, T.M.: Applying formal specification in industry. IEEE Softw. 13(3), 48\u201356 (1996)","journal-title":"IEEE Softw."},{"key":"750_CR36","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: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Proceedings ABZ, pp.\u00a0335\u2013350. Springer, Cham (2020)"},{"key":"750_CR37","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1145\/2950290.2950318","volume-title":"Proceedings ACM SIGSOFT, FSE 2016","author":"N. Macedo","year":"2016","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: Proceedings ACM SIGSOFT, FSE 2016, pp.\u00a0373\u2013383. Association for Computing Machinery, New York (2016)"},{"key":"750_CR38","first-page":"367","volume-title":"Proceedings ABZ","author":"A. Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M.: Modeling of a speed control system using event-B. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Proceedings ABZ, pp.\u00a0367\u2013381. Springer, Cham (2020)"},{"key":"750_CR39","first-page":"351","volume-title":"Proceedings ABZ","author":"A. Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M., Laleau, R.: An event-B model of an automotive adaptive exterior light system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Proceedings ABZ, pp.\u00a0351\u2013366. Springer, Cham (2020)"},{"key":"750_CR40","unstructured":"MISRA C:2012 \u2013 Guidelines for the use of the C language in critical systems. MISRA (2013)"},{"issue":"7","key":"750_CR41","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, M.J.: Assessment of high-integrity embedded automotive control systems using hardware in the loop simulation. J. Syst. Softw. 81(7), 1163\u20131183 (2008)","journal-title":"J. Syst. Softw."},{"key":"750_CR42","first-page":"456","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, pp.\u00a0456\u2013473. Springer, Berlin (2019)"},{"key":"750_CR43","series-title":"LNCS","first-page":"290","volume-title":"Combining Formal and Informal Methods in the Design of Spacecrafts","author":"M. Yang","year":"2016","unstructured":"Yang, M., Zhan, N.: Combining Formal and Informal Methods in the Design of Spacecrafts. LNCS, vol.\u00a09506, pp.\u00a0290\u2013323. Springer, Berlin (2016)"},{"key":"750_CR44","first-page":"376","volume-title":"Proceedings CAV, LNCS","author":"J. Yuan","year":"1997","unstructured":"Yuan, J., Shen, J., Abraham, J., Aziz, A.: On combining formal and informal verification. In: Proceedings CAV, LNCS, vol.\u00a01254, pp.\u00a0376\u2013387. Springer, Berlin (1997)"}],"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-00750-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00750-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00750-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T02:34:07Z","timestamp":1732070047000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00750-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,27]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["750"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00750-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,27]]},"assertion":[{"value":"29 April 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}