静态分析真的是形式验证吗？

Question

我一直在阅读关于形式验证的文章，基本点是它需要一个正式的规范和模型来使用。然而，许多来源将静态分析归类为形式验证技术，有些提到抽象解释并提到它在编译器中的使用。所以我很困惑 - 如果没有模型的正式描述，这些如何进行形式验证？
编辑：我发现的一个来源是：

静态分析：根据预定义的抽象（有时可以由用户自动/手动定制）从程序文本中自动计算抽象语义

那么这是否意味着它只适用于源代码而无需正式规范？这就是静态分析器所做的。

另外，在没有形式验证的情况下可以进行静态分析吗？例如，SonarQube 真的执行形式化方法吗？

Answer 1

在硬件和软件系统的背景下，形式验证是使用形式数学方法证明或反驳系统底层预期算法相对于某种形式规范或属性的正确性的行为。

如果没有模型的正式描述，如何进行形式化验证？

静态分析器将生成一段代码的控制/数据流，然后可以应用形式化方法来验证是否符合系统/单元的预期设计模型。

请注意，建模/形式规范不是静态分析的一部分。
不管怎样组合在一起，这两种工具在形式验证中都很有用。

例如，如果系统被建模为有限状态机 (FSM)

• 由某些成员数据的特定值的组合定义的预定义数量的状态。
  
• 由成员函数列表定义的各种状态之间的预定义转换集。
  

然后，静态分析的结果将有助于形式化验证以下事实：
控制永远不会沿着上述 FSM 模型中不存在的路径流动。

此外，如果可以根据类型定义、数据流、控制流/调用图（即静态分析器可以验证的代码度量）简单地定义模型，那么静态分析本身就足以正式验证该代码符合这样的模型。

_{注1。上面的黄色区域是静态分析器，用于强制执行诸如编码指南和命名约定之类的内容，即不能影响程序行为的代码方面。}

_{笔记2。上面的红色区域是形式验证，需要额外的步骤，例如 100% 动态代码覆盖、消除未使用的代码和死代码。这些无法使用静态分析器检测/强制执行。}

静态分析对于验证系统/单元是否使用语言规范的子集实现以满足系统/单元设计中规定的目标非常有效。

例如，如果设计目标是防止堆栈内存超过特定限制，则可以对递归深度应用限制（或完全禁止递归函数调用）。静态分析用于识别此类违反设计目标的行为。

在没有来自静态分析器的任何警告的情况下，
系统/单元代码根据其各自模型的此类设计目标进行正式验证。

例如。汽车软件 MISRA-C 标准定义了用于汽车系统的 C 子集。

MISRA-C:2012 包含

• 143 条规则- 每条规则都可以使用静态程序分析进行检查。

• 16 个“指令”更易于解释，或与流程相关。