符号状态探索在符号模型检查中的工作原理答案

【问题标题】：How the Symbolic State Exploration works in Symbolic Model Checking符号状态探索在符号模型检查中的工作原理
【发布时间】：2018-05-30 02:55:44
【问题描述】：

以下algorithm 是使用Computational Tree Logic (CTL) 进行模型检查的粗略草图：

据说：

CTL 的模型检查问题是验证给定过渡系统 TS 和 CTL 公式 Φ 是否 TS |= Φ... CTL 模型检查的基本过程相当简单：

满足 Φ 的所有状态的集合 Sat(Φ) 是递归计算的，并且

TS |= Φ 当且仅当 I ⊆ Sat(Φ) 其中 I 是 TS 的初始状态集...

Sat(Φ) 的递归计算基本上归结为 CTL 状态公式 Φ 的解析树的自下而上遍历。

所以你本质上（根据我的理解），你为系统提供了一个 CTL 公式 Φ，它是一个解析树，然后它搜索状态，并通过 CTL 解析树，并检查是否有任何状态满足 Φ .

问题是：

在 Sat(Φ) 方法中，大致会发生什么（象征性的东西）。他们在下面说（2），其中 S 是状态，A 是原子命题。想知道他们是如何实际检查状态的，考虑到程序实际上并没有运行。这是（至少我认为）符号模型检查。想知道是否可以大致解释状态检查的工作原理。似乎某种input generation 必须发生，但同时我想也许它不应该发生。

对我来说很难理解的原因是这个。假设其中一个断言是针对一个函数addTricky(x, y)，它的实现方式如下：

function addTricky(x, y) {
  if (y >= 1) return 3
  return x + y
}

然后我会有一个 布尔表达式 在某些逻辑中说“在 addTricky 之前：z = 0。在 z = addTricky(x, y) 之后：y >= 1 -> z = 3; y

基本上试图解决模式的问题。如果 Sat(Φ) 基本上在做我刚才在那个布尔表达式中所做的事情，我想知道它是否曾经调用/调用函数 addTricky，或者它是否可以以某种方式象征性地完成这一切。我还没有看到它是如何工作的，想知道是否可以解释一下符号执行的基本原理。对我来说，我一直在想象它进行某种单元测试，例如插入addTricky(1, 1)，并检查所有可能性。也许那是“显式状态探索”与符号探索，不确定。

非常感谢您的帮助！

(1) 对于解析树的每个节点，即对于 Φ 的每个子公式 Ψ，计算满足 Ψ 的状态集 Sat(Ψ)。

(2) Sat(a) = {s ∈ S | a ∈ L(s)}, for any a ∈ A

【问题讨论】：

标签： algorithm logic formal-verification model-checking

【解决方案1】：

我认为您的问题有两个部分：1）如何从软件功能转到过渡系统，以及 2）如何使用过渡系统来检查满意度。

1) 转移系统基本上是有限状态自动机的扩展。如果您有您描述的功能，您首先需要将其转换为转换系统。例如，这可以通过为代码的每个可执行行引入状态，以及遵循代码条件的状态之间的转换来完成。在转换系统级别，您没有函数调用的概念，因此您需要在翻译过程中注意这一点，例如，通过内联函数定义。此步骤与您如何验证转换系统无关。正如您可以想象的那样，这可能会导致相当大的过渡系统。

还有其他不基于转换系统的方法，它们模拟程序的执行并在此过程中收集符号约束。符号执行就是这样一个例子。

2) 假设您内联了 addTricky 函数并得到了一些类似的东西

L0: z=0
    if (y>=1)
L1:     z=3
    else
L2:     z=x+y

一个可能的 TS 是：

(L0: z=0) --[y >= 1]--> (L1: z=3) 
    |
  [y<1]
   \/
(L2: z=x+y)

您有 3 个可执行语句，这导致 TS 的符号状态 (S) 为：

 L0: Z=0; X=?; Y=?
 L1: Z=3; X=?; Y>=1
 L2: Z=X+Y; X=?; Y<1

在哪里？表示任何值。这种方法的强大之处在于，您可以在单个符号状态下紧凑地表示 X 和 Y 的所有值。

【讨论】：