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

Sebastian Krings, Philipp Koerner, Jannik Dunkelau, Chris Rutenkolk
Case Study Digital Printed Abstract View Cite Source
Type
Conference paper
Publication
7th International Conference on Rigorous State Based Methods (ABZ'20)

Abstract

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.

Document

Reference

% BibTex
@inproceedings{krings2020abz,
  title={{A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System}},
  author={Krings, Sebastian and Koerner, Philipp and Dunkelau, Jannik and Rutenkolk, Chris},
  booktitle={7th International Conference on Rigorous State Based Methods (ABZ'20)},
  pages={382--397},
  year={2020},
  organization={Springer}
}

Sources

  • Used formal method: MISRA C

    For more information, please contact the authors

ABZ'20

Related