Annotating Control-Flow Graphs for Formalized Test Coverage Criteria

控制流覆盖准则是为安全关键系统的嵌入式软件进行合格性认证过程中的重要组成部分。类似DO-178B中定义的修改条件/决策覆盖（MC/DC）等准则被监管机构用于判断测试的充分性，同时也被QA工程师用于设计测试，当全路径覆盖不可能时。尽管它们很重要，但这些覆盖准则经常被误解。一个问题是它们的定义通常是用自然语言规范文件编写的，使它们不够精确。其他作品提出了使用二元谓词逻辑的形式定义，但这些定义很难应用于实际程序的分析。控制流图（CFGs）是编译器中分析程序逻辑的最常见模型，并且似乎非常适合定义和分析覆盖准则。然而，CFGs舍弃了决策的明确概念，使得它们似乎无法用于此任务。在本文中，我们展示了如何从图本身推断出决策信息来注释CFG。我们称这个带注释的模型为控制流决策图（CFDG），并使用它来形式化定义几个常见的覆盖准则。我们已经在一个工具中实现了我们的算法，并展示了它可以自动注释从流行编译器输出的CFG。

CFDGs are a good fit for defining and analyzing coverage criteria, but they discard the explicit concept of a decision, making their use for this task seem impossible. This paper aims to annotate a CFG with decision information inferred from the graph itself to solve this problem.

The paper proposes the concept of Control-Flow Decision Graphs (CFDGs) to annotate CFGs with decision information, allowing for the formal definition and analysis of common coverage criteria. An algorithm and tool have been implemented to automatically annotate CFGs output from popular compilers.

The paper's proposed CFDGs and algorithm provide a more precise and automated way to define and analyze control flow coverage criteria. The tool's implementation makes it easy to apply the proposed method to real-world programs. The paper also compares the proposed method to previous formal definitions and shows its advantages.

Related work includes previous formal definitions of control flow coverage criteria using binary predicate logic, as well as research on other methods for analyzing program logic in compilers.