Annotating Control-Flow Graphs for Formalized Test Coverage Criteria

TL;DR

This work addresses imprecision in control-flow coverage criteria by introducing Control-Flow Decision Graphs ($CFDGs$), an annotated CFG model that makes decisions explicit. It provides algorithms to automatically transform CFGs into CFDGs, proves correctness and linear-time complexity, and formalizes common criteria such as SC, DC, CC, MCC, FPC, and MC/DC within this model. An open-source tool, cfg2cfdg, annotates CFGs from GCC and Clang, enabling automated, visually comparable CFDGs. The approach facilitates precise reasoning and practical test-design guidance for safety-critical software, bridging theory and real-world compiler outputs.

Abstract

Control flow coverage criteria are an important part of the process of qualifying embedded software for safety-critical systems. Criteria such as modified condition/decision coverage (MC/DC) as defined by DO-178B are used by regulators to judge the adequacy of testing and by QA engineers to design tests when full path coverage is impossible. Despite their importance, these coverage criteria are often misunderstood. One problem is that their definitions are typically written in natural language specification documents, making them imprecise. Other works have proposed formal definitions using binary predicate logic, but these definitions are difficult to apply to the analysis of real programs. Control-Flow Graphs (CFGs) are the most common model for analyzing program logic in compilers, and seem to be a good fit for defining and analyzing coverage criteria. However, CFGs discard the explicit concept of a decision, making their use for this task seem impossible. In this paper, we show how to annotate a CFG with decision information inferred from the graph itself. We call this annotated model a Control-Flow Decision Graph (CFDG) and we use it to formally define several common coverage criteria. We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.

Figures (4)

• Figure 1: Possible runs of the program in Listing \ref{['lst:scand']}
• Figure 2: Steps of Algorithms \ref{['alg:init']} and \ref{['alg:alg']} on the CFG for Listing \ref{['lst:three']}
• Figure 3: Parts of a visualized CFG output from Clang annotated using cfg2cfdg
• Figure 4: Parts of a visualized CFG output from GCC annotated using cfg2cfdg

Theorems & Definitions (14)

• Lemma 1: Outdegree of Decision Subgraphs
• proof
• Lemma 2: Indegree of Decision Subgraphs
• proof
• Theorem 1: Shared Successors of Conditions in a Decision
• proof
• Theorem 2: Soundness
• proof
• Theorem 3: Completeness
• proof