形式化验证

在硬件和软件系统的背景下，形式化验证是使用数学的形式化方法，证明或反驳系统所依据的预定算法在某种形式化规范或属性方面的正确性的行为。形式化验证有助于证明系统的正确性，例如：加密协议、组合电路、带有内部存储器的数字电路以及以源代码形式表达的软件。这些系统的验证是通过在系统的抽象数学模型上提供形式化证明来完成的，数学模型和系统的性质之间的对应关系是通过构造知道的。经常用于系统建模的数学对象的例子有：有限状态机、标记过渡系统、Petri网、向量加法系统、定时自动机、混合自动机、过程代数、编程语言的形式语义，如操作语义、指称语义、公理语义和Hoare逻辑。

一种方法和形成是模型检查，它包括对数学模型进行系统的详尽探索（这对有限模型来说是可能的，但对一些无限模型来说也是可能的，因为无限的状态集可以通过使用抽象或利用对称性而有效地被有限地表示）。通常，这包括探索模型中的所有状态和转换，通过使用智能和特定领域的抽象技术，在一次操作中考虑整组状态并减少计算时间。实施技术包括状态空间枚举、符号状态空间枚举、抽象解释、符号模拟、抽象细化。要验证的属性通常用时间逻辑描述，如线性时间逻辑（LTL）、属性规范语言（PSL）、SystemVerilog断言（SVA）或计算树逻辑（CTL）。模型检查的xxx优点是它通常是全自动的；它的主要缺点是它一般不能扩展到大型系统；符号模型通常被限制在几百比特的状态，而显式状态枚举要求被探索的状态空间相对小。另一种方法是演绎验证。它包括从系统和它的规范（可能还有其他注释）中生成数学证明义务的集合，这些义务的真实性意味着系统符合其规范，并使用证明助手（交互式定理证明器）（如HOL、ACL2、Isabelle、Coq或PVS）或自动定理证明器来履行这些义务，特别是包括可满足性模数理论（SMT）解决器。这种方法的缺点是，它可能需要用户详细了解系统正确工作的原因，并将这些信息传达给验证系统，其形式可以是有待证明的定理序列，也可以是系统组件（如函数或程序）和可能的子组件（如循环或数据结构）的规范（不变量、前提条件、后置条件）。

软件程序的形式化验证包括证明一个程序满足其行为的形式化规范。形式化验证的子领域包括演绎验证（见上文）、抽象解释、自动定理证明、类型系统和轻型形式化方法。一个有前途的基于类型的验证方法是依赖类型的编程，其中函数的类型包括（至少是部分）这些函数的规范，类型检查代码根据这些规范建立其正确性。全功能的依赖类型语言作为一种特殊情况支持演绎验证。另一种补充方法是程序推导，通过一系列保持正确性的步骤，从功能规范中产生有效的代码。这种方法的一个例子是Bird-Meertens形式主义，这种方法可以被看作是另一种形式的构造正确性。

这些技术可以是健全的，也就是说，被验证的属性可以从语义中逻辑推导出来，或者是不健全的，也就是说，没有这样的保证。健全的技术只有在覆盖了整个可能性的空间之后才会产生结果。一个不健全的技术的例子是，它只覆盖了可能性的一个子集，例如只覆盖了某个数字以下的整数，并给出了一个足够好的结果。技术也可以是可判定的，也就是说，它们的算法实现可以保证以一个答案结束，或者是不可判定的，也就是说，它们可能永远不会结束。通过限定可能性的范围，当没有可判定的健全技术可用时，可判定的不健全技术就能够被构造出来。