Dokument: A verified low-level implementation and visualization of the adaptive exterior light and speed control system
| Titel: | A verified low-level implementation and visualization of the adaptive exterior light and speed control system | |||||||
| URL für Lesezeichen: | https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=68187 | |||||||
| URN (NBN): | urn:nbn:de:hbz:061-20250121-103017-9 | |||||||
| Kollektion: | Publikationen | |||||||
| Sprache: | Englisch | |||||||
| Dokumententyp: | Wissenschaftliche Texte » Artikel, Aufsatz | |||||||
| Medientyp: | Text | |||||||
| Autoren: | Krings, Sebastian [Autor] Körner, Philipp [Autor] Dunkelau, Jannik [Autor] Rutenkolk, Kristin [Autor] | |||||||
| Dateien: |
| |||||||
| Stichwörter: | Case study, Formal methods, Verification, Model checking, MISRA C, Test-driven development | |||||||
| Beschreibung: | 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. | |||||||
| Rechtliche Vermerke: | Originalveröffentlichung:
Krings, S., Körner, P., Dunkelau, J., & Rutenkolk, K. (2024). A verified low-level implementation and visualization of the adaptive exterior light and speed control system. International Journal on Software Tools for Technology Transfer, 26(3), 403–419. https://doi.org/10.1007/s10009-024-00750-5 | |||||||
| Lizenz: |  Dieses Werk ist lizenziert unter einer Creative Commons Namensnennung 4.0 International Lizenz | |||||||
| Fachbereich / Einrichtung: | Mathematisch- Naturwissenschaftliche Fakultät | |||||||
| Dokument erstellt am: | 21.01.2025 | |||||||
| Dateien geändert am: | 21.01.2025 |
