A Novel Approach in Proving Unreachable Paths in Hardware-Dependent Software

EasyChair Preprint 14768

Abstract

Achieving reliable code coverage is of fundamental importance in embedded systems development, especially in compliance with automotive standards like ISO26262. Firmware designs, with their hardware interaction, require thorough testing to minimize the risk of undetected bugs. Achieving 100% code coverage is challenging. This paper adds a step in the development process to detect unreachable paths in the initial phase of the development process. This paper proposes a methodology using MC/DC (Modified Condition Decision Coverage) with formal verification to analyze code functions individually within a time-bound. The paper presents the common bugs found in 7 firmware designs. For example in a FW design with 16k lines of code, 51 of 613 paths were unreachable, with 25 paths being due to bugs. Before addressing initial bugs, 1332 potential software weaknesses were identified using formal verification, which increased to 1370 after correction. It shows the benefits of including the detection of unreachable paths and avoiding, later corrections during integration.

Keyphrases: Firmware verification, code coverage, formal verification

@booklet{EasyChair:14768,
  author    = {Bryan Daniel Olmos Suquillo and Wolfgang Kunz and Djones Lettnin},
  title     = {A Novel Approach in Proving Unreachable Paths in Hardware-Dependent Software},
  howpublished = {EasyChair Preprint 14768},
  year      = {EasyChair, 2024}}