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

【问题标题】：Is static analysis really formal verification?静态分析真的是形式验证吗？
【发布时间】：2016-06-02 16:28:41
【问题描述】：

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

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

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

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

【问题讨论】：

【解决方案1】：

在硬件和软件系统的上下文中，形式验证是证明或反驳预期算法的正确性的行为关于某个形式规范或属性的系统底层，使用形式化方法数学。

如果没有模型的正式描述，这些怎么可能是形式验证？

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

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

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

那么静态分析的结果将有助于形式化验证
控制永远不会沿着上述 FSM 模型中不存在的路径流动。

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

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

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

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

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

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

例如。 MISRA-C standard for Automotive software 定义了用于汽车系统的 C 子集。

MISRA-C:2012 包含

【讨论】：

谢谢，例如SonarQube 使用形式化方法？因为我从来没有读过这样的东西
@user970696 我找不到 SonarQube 使用正式方法的任何文档。但是，类似的工具Goanna makes an explicit claim about using formal methods alongwith its static-analyser。
@TheCodeArist 问题是，如果 Sonar 不使用形式化方法，它会做静态分析吗？由于含义不清楚，我发现它令人困惑。
是的。 Sonar 进行静态分析。如果您还需要对您的软件进行形式验证，那么您将需要执行额外的步骤，例如定义模型和使用形式方法来验证代码是否符合模型。您可以使用 SonarQube 的静态分析结果作为形式验证方法的输入。此外，如果模型可以简单地根据控制流/调用图来定义，那么静态分析本身就足以正式验证模型。
正如我所提到的，有些书或文章说“静态分析”是一种形式化方法，这令人困惑。如果我没记错的话，Sonar 也可以检测到一些“设计”错误，这不适合纯静态分析。

【解决方案2】：

静态分析只是意味着“阅读源代码并可能抱怨”。（与“动态分析”相反，意思是“运行程序并可能抱怨某些执行行为”）。

有很多不同类型的可能的静态分析投诉。一种可能的抱怨可能是，

 Your source code does not provably satisfy a formal specification

如果静态分析器具有“正式”解释的正式规范、源代码的正式解释以及无法找到合适定理的可信定理证明器，则此投诉将基于形式验证。

您可能从静态分析器中得到的所有其他类型的抱怨几乎都是启发式意见，也就是说，它们是基于对代码（或规范，如果它确实存在的话）的一些非正式解释。

Coverity 等“重型”静态分析器具有相当不错的程序模型，但它们不会告诉您您的代码是否符合规范（它们甚至不会查看您是否有规范）。充其量他们只会告诉您您的代码根据语言做了一些未定义的事情（“取消引用空指针”），甚至这种抱怨并不总是正确的。

诸如 MISRA 之类的所谓“样式检查器”也是静态分析器，但它们的抱怨本质上是“您使用了某个委员会认为格式错误的构造”。这实际上不是错误，纯属意见。

【讨论】：

【解决方案3】：

您当然可以将静态分析归类为一种形式验证。

如果没有模型的正式描述，这些怎么可能是形式验证？

对于静态分析工具，模型是隐式的（或在某些工具中是部分隐式的）。例如，“格式良好的 C++ 程序不会泄漏内存，也不会访问尚未初始化的内存”。这些规则可以来自语言规范，或者来自特定项目的编码标准。

【讨论】：