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.

翻译：控制流覆盖准则是安全关键系统嵌入式软件认证过程中的重要组成部分。当完整路径覆盖无法实现时，监管机构采用DO-178B定义的修订条件/判定覆盖（MC/DC）等准则来评估测试的充分性，质量保证工程师则依据这些准则设计测试用例。尽管这些覆盖准则至关重要，却常被误解。问题之一在于其定义通常以自然语言规范文档的形式呈现，导致表述不够精确。已有研究提出采用二元谓词逻辑的形式化定义，但这些定义难以应用于实际程序的分析。控制流图是编译器中分析程序逻辑最常用的模型，似乎适合用于定义和分析覆盖准则。然而，控制流图舍弃了判定的显式概念，使其在这项任务中的应用看似不可行。本文展示了如何通过从图结构本身推断判定信息来标注控制流图。我们将这种标注模型称为控制流判定图，并利用它形式化定义了几种常见覆盖准则。我们已将相关算法实现为工具，该工具可自动标注主流编译器输出的控制流图。