A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System

In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) approach following a formal method, we use MISRA C for a low-level implementation instead. We strictly adhere to test-driven developm...

Descripción completa

Detalles Bibliográficos
Autores principales: Krings, Sebastian, Körner, Philipp, Dunkelau, Jannik, Rutenkolk, Chris
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7242055/
http://dx.doi.org/10.1007/978-3-030-48077-6_30
_version_ 1783537171791085568
author Krings, Sebastian
Körner, Philipp
Dunkelau, Jannik
Rutenkolk, Chris
author_facet Krings, Sebastian
Körner, Philipp
Dunkelau, Jannik
Rutenkolk, Chris
author_sort Krings, Sebastian
collection PubMed
description In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) approach following a formal method, we use MISRA 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. In consequence, our realization of the ABZ case study can serve as a baseline reference for comparison, allowing to assess the benefit provided by the various formal modeling languages, methods and tools.
format Online
Article
Text
id pubmed-7242055
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72420552020-05-22 A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System Krings, Sebastian Körner, Philipp Dunkelau, Jannik Rutenkolk, Chris Rigorous State-Based Methods Article In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) approach following a formal method, we use MISRA 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. In consequence, our realization of the ABZ case study can serve as a baseline reference for comparison, allowing to assess the benefit provided by the various formal modeling languages, methods and tools. 2020-04-22 /pmc/articles/PMC7242055/ http://dx.doi.org/10.1007/978-3-030-48077-6_30 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Krings, Sebastian
Körner, Philipp
Dunkelau, Jannik
Rutenkolk, Chris
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
title A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
title_full A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
title_fullStr A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
title_full_unstemmed A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
title_short A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
title_sort verified low-level implementation of the adaptive exterior light and speed control system
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7242055/
http://dx.doi.org/10.1007/978-3-030-48077-6_30
work_keys_str_mv AT kringssebastian averifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT kornerphilipp averifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT dunkelaujannik averifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT rutenkolkchris averifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT kringssebastian verifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT kornerphilipp verifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT dunkelaujannik verifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem
AT rutenkolkchris verifiedlowlevelimplementationoftheadaptiveexteriorlightandspeedcontrolsystem

Ejemplares similares