For Publishers
DiscoveryMetadataPeer reviewHostingPublishing
For Researchers
JoinPublishReviewCollect
Register
Blog
About
Search
Advanced search
My ScienceOpen
Search
For Publishers
For Researchers
Blog
About
1
views
11
references
 Top references
cited by
0
    
0 reviews
 Review
0
comments
 Comment
0
recommends
+1 Recommend
0 collections
    0
    shares
      85
      similar
       All similar
      • Record: found
      • Abstract: found
      • Article: not found

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

      chapter-article

      Read this article at

      ScienceOpenPublisherPMC
      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references11

          • Record: found
          • Abstract: not found
          • Article: not found

          Seven more myths of formal methods

          J.P. Bowen, M.G. Hinchey, Jonathan Bowen (1995)
          Article 0 comments Cited 19 times – based on 0 reviews     Review now
            Bookmark
            • Record: found
            • Abstract: not found
            • Conference Proceedings: not found

            A tool for checking ANSI-C programs

            E. CLARKE, D. Kroening, F Lerda … (2004)
            Article 0 comments Cited 5 times – based on 0 reviews
              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Language subsetting in an industrial context: A comparison of MISRA C 1998 and MISRA C 2004

              Les Hatton (2007)
              Article 0 comments Cited 2 times – based on 0 reviews     Review now
                Bookmark
                All references

                Author and article information

                Contributors
                Alexander Raschke: alexander.raschke@uni-ulm.de
                Dominique Méry: dominique.mery@loria.fr
                Frank Houdek: frank.houdek@daimler.com
                Sebastian Krings:
                ORCID: http://orcid.org/0000-0001-6712-9798
                sebastian@krin.gs
                Philipp Körner:
                ORCID: http://orcid.org/0000-0001-7256-9560
                p.koerner@hhu.de
                Jannik Dunkelau:
                ORCID: http://orcid.org/0000-0003-0819-5554
                jannik.dunkelau@hhu.de
                Chris Rutenkolk:
                ORCID: http://orcid.org/0000-0002-6751-0369
                chris.rutenkolk@hhu.de
                Journal
                Journal ID (publisher-id): 978-3-030-48077-6
                Journal ID (doi): 10.1007/978-3-030-48077-6
                Journal ID (nlm-ta): Rigorous State-Based Methods
                Title: Rigorous State-Based Methods
                Subtitle: 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020, Proceedings
                ISBN (Print): 978-3-030-48076-9
                ISBN (Electronic): 978-3-030-48077-6
                Publication date (Electronic): 22 April 2020
                Volume: 12071
                Pages: 382-397
                Affiliations
                [8 ]GRID grid.6582.9, ISNI 0000 0004 1936 9748, Institute of Software Engineering and Programming Languages, , Ulm University, ; Ulm, Germany
                [9 ]GRID grid.29172.3f, ISNI 0000 0001 2194 6418, LORIA, Campus Scientifique, , Université de Lorraine, ; Vandoeuvre-les-Nancy, France
                [10 ]GRID grid.410308.e, ISNI 0000 0004 0572 0912, Research and Development, , Mercedes-Benz AG, ; Sindelfingen, Germany
                [11 ]GRID grid.440943.e, ISNI 0000 0000 9422 7759, Institute for Information Security, , Niederrhein University of Applied Sciences, ; Mönchengladbach, Germany
                [12 ]GRID grid.411327.2, ISNI 0000 0001 2176 9917, Institut für Informatik, , Heinrich-Heine-Universität, ; Universitätsstr. 1, 40225 Düsseldorf, Germany
                Author information
                http://orcid.org/0000-0001-6712-9798
                http://orcid.org/0000-0001-7256-9560
                http://orcid.org/0000-0003-0819-5554
                http://orcid.org/0000-0002-6751-0369
                Article
                Publisher ID: 30
                DOI: 10.1007/978-3-030-48077-6_30
                PMC ID: 7242055
                SO-VID: 24691013-fd7f-4683-bfe8-e92208d32d2b
                Copyright © © Springer Nature Switzerland AG 2020
                License:

                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.

                History
                Categories
                Subject: Article
                Custom metadata
                issue-copyright-statement © Springer Nature Switzerland AG 2020

                Data availability:

                Comments

                Comment on this article