形式验证

在硬件和软件系统的上下文中，形式验证是使用形式数学方法证明或反驳系统下针对特定形式规范或属性的预期算法的正确性的行为。

形式验证可以帮助证明系统的正确性，例如：密码协议、组合电路、带有内部存储器的数字电路以及表示为源代码的软件。

这些系统的验证是通过对系统的抽象数学模型提供正式证明来完成的，数学模型与系统性质之间的对应关系通过构造已知。 经常用于对系统建模的数学对象的例子有：有限状态机、标记转换系统、Petri 网、向量加法系统、时间自动机、混合自动机、过程代数、编程语言的形式语义，例如操作语义、指称语义、公理化 语义和霍尔逻辑。

一种方法和形式是模型检查，它包括对数学模型的系统详尽探索（这对于有限模型是可能的，但对于一些无限模型也是可能的，其中无限状态集可以通过使用抽象或利用 对称）。 通常，这包括探索模型中的所有状态和转换，通过使用智能和特定领域的抽象技术在单个操作中考虑整个状态组并减少计算时间。 实现技术包括状态空间枚举、符号状态空间枚举、抽象解释、符号模拟、抽象细化。 要验证的属性通常在时态逻辑中描述，例如线性时态逻辑 (LTL)、属性规范语言 (PSL)、SystemVerilog 断言 (SVA) 或计算树逻辑 (CTL)。 模型检查的xxx优点是它通常是全自动的； 它的主要缺点是它通常不能扩展到大型系统； 符号模型通常仅限于几百位状态，而显式状态枚举则需要探索的状态空间相对较小。

另一种方法是演绎验证。 它包括从系统及其规范（以及可能的其他注释）生成数学证明义务的集合，其真实性意味着系统符合其规范，并使用证明助手（交互式定理证明者）履行这些义务（ 例如 HOL、ACL2、Isabelle、Coq 或 PVS）或自动定理证明器，尤其包括可满足性模理论 (SMT) 求解器。 这种方法的缺点是它可能需要用户详细了解系统为何正确工作，并将此信息以要证明的定理序列的形式或规范的形式传递给验证系统（ 系统组件（例如函数或过程）和可能的子组件（例如循环或数据结构）的不变量、前提条件、后置条件）。

软件程序的形式验证涉及证明程序满足其行为的正式规范。 形式验证的子领域包括演绎验证（见上文）、抽象解释、自动定理证明、类型系统和轻量级形式方法。 一种有前途的基于类型的验证方法是依赖类型编程，其中函数的类型包括（至少部分）那些函数的规范，并且类型检查代码确定其针对这些规范的正确性。 功能齐全的依赖类型语言支持演绎验证作为一种特殊情况。

另一种补充方法是程序推导，其中通过一系列正确性保持步骤从功能规范中生成高效代码。 这种方法的一个例子是 Bird-Meertens 形式主义，这种方法可以看作是另一种形式的构造正确性。

这些技术可以是可靠的，这意味着可以从语义中逻辑推导出已验证的属性，也可以是不可靠的，这意味着没有这样的保证。 一项完善的技术只有在覆盖了所有可能性的情况下才会产生结果。 不健全技术的一个例子是仅涵盖可能性的子集，例如仅涵盖特定数量的整数，并给出足够好的结果。 技术也可以是可判定的，这意味着它们的算法实现保证以答案终止，或者是不可判定的，这意味着它们可能永远不会终止。 通过限制可能性的范围，当没有可判定的可靠技术可用时，可以构建可判定的不可靠技术。