Python：寻找模型检查工具及其转CNF的结果

1 投票

1 回答

2228 浏览

数据工程师

提问于 2025-04-18 08:17

我想用模型检查器来测试我的代码，并自动生成一个有限状态机（FSM）。为此，我需要一个模型检查器，并把FSM的结果转换成CNF格式。

有没有什么建议可以让我在Python中做到这一点？我只知道CBMC，但它只支持C语言。

谢谢，
阿德里安

自动化测试代码验证有限状态机模型检查 cnf格式

1 个回答

Python 这种语言并不适合用来做模型检查。比如说，鸭子类型让我们在处理异常时有很多自由。如果你的 Python 代码基本上是过程式编程，那么你可以先尝试用 C 转换它，使用 py2c 或类似的工具。

然后用 modex 从 C 代码中提取一个 Promela 模型。这个最后的步骤叫做抽象。接下来，你可以使用 SPIN 模型检查器来验证你关心的属性。

如果 CNF 是指 "合取范式"，那么我不明白 CNF 和模型检查的结果有什么关系。模型检查的结果要么是：

"是的，你的模型符合你提供的逻辑公式"，或者
"不符合，这里有一个反例说明为什么不符合"。

CNF 是一种特定的语法形式，用于布尔公式。

如果你提到 CNF 和 CBMC 相关的有界模型检查，以及涉及的 SAT 求解，那么请注意，SPIN 接受的输入是用 Promela 语言表达的 Kripke 模型。所以你不需要把任何东西转换成布尔公式，另外你还可以进行完整的活性验证检查。

这个工具列表包含了模型检查器。特别是，如果你想写一个从 Python 转换到 Promela 的转换器，那么你可能会觉得以下内容很有用：

ast 模块：这是 CPython 标准库的一部分，用于 Python 语言的抽象语法树（这个树是通过 CPython 的解析器构建的）
promela Python 包：用于 Promela 的解析器和抽象语法树，使用 Python 实现
promela-metamodel
ocaml 库用于 promela
pi2promela
程序到 Promela 的转换器.

另外，注意 "FSM"（有限状态机）是一个 转换器，而不是 Kripke 结构。转换器有输入和输出。它对输入做出反应，产生输出。它是在对抗环境中合成的结果，其中有一个环境（控制输入）和一个系统（控制输出），并且希望合成一个满足某些以逻辑公式表达的规范的策略。解决这个问题的工具有很多。结果是一个 Mealy 机，或者一个 Moore 机（它们是不同的，不是等价的），这两者都是转换器的类型。

转换器不是 Kripke 结构（或者说转移系统，尽管后者的术语通常用得不太准确，所以最好称之为 Kripke 结构或模型，可以用图表示，节点用你在逻辑公式中提到的命题标记）。

观察合成和验证（模型检查是一种验证形式）之间的区别：

封闭系统合成（没有环境）接受一个公式，并合成一个满足该公式的模型，形式是 Kripke 结构。
封闭系统验证接受一个模型和一个期望的公式，然后检查该模型是否满足规范。

封闭系统合成也可以使用 "部分" 模型进行，这意味着模型是对公式的额外约束。在这种情况下，合成的结果必须同时满足公式并且是部分模型的 "子模型"。

开放系统合成可以使用逻辑公式作为输入，然后通过解决系统和环境之间的博弈，我们获得一个 转换器，它实现了一个策略，使得系统能够满足逻辑公式，而不管环境如何选择（前提是环境遵守逻辑公式）。

注意以下两者之间的区别：

在开放系统合成中相关的转换器（FSM），和
作为封闭系统合成输入的有限转移系统（FTS）或 Kripke 结构。

顺便提一下，模型检查器通常接受封闭系统作为输入，因此在封闭系统设置中建模环境必须通过在转移系统中引入不受控制的非确定性来完成。

关于开放和封闭系统、公式、有限-状态机、有限转移系统、合成和验证的上述描述，可以用 TLA+ 以简单和统一的方式理解：

公式是布尔值表达式，例如公式：
- a /\ ~ b 和
- (x = 1) /\ (y \in Nat).
有限状态机和有限转移系统实际上没有什么不同，它们只是 (时间) 公式的语法糖
通常不同的是我们在验证中如何使用图状结构，以及在合成中如何使用它们：
- 在验证中，描述系统可以采取哪些步骤（转移）的图状结构有时称为 "有限转移系统"。它是验证的输入。
- 在合成中，描述当系统环境（世界的其余部分）发生某些变化时，系统（受控部分）如何变化的（合成的）图状结构，有时称为 "有限状态机"。
有限状态机这个术语可以指有限转移系统。关键是我们通过指定 "状态" 如何变化来描述世界。这个概念并不限于有限结构。因此，写 "状态机" 就足够了。
非正式地说，封闭系统是可以用一组值描述的世界部分的行为集合。
非正式地说，开放系统是可以描述的世界部分的行为集合，包括不受限制的行为：即任何违反环境假设的行为。
验证是量词消除，在一个带有单个量词的公式中进行。换句话说，如果：
- 操作符 System(variable) 描述系统在变量 variable 下的行为，并且
- 操作符 Specification(variable) 描述期望的系统行为，
那么验证就是证明公式 \AA variable: System(variable) => Specification(variable) 是一个定理的活动：
```
THEOREM \AA variable:  System(variable) => Specification(variable)
```
用简单的话来说，这个定理表明，对于变量 variable 的所有时间演变，如果公式 System(variable) 在某个演变中为 TRUE，那么公式 Specification(variable) 在该演变中也为 TRUE。

为了与上述关于有限转移系统和模型检查的描述相连接：
- 公式 System(variable) 在谓词逻辑、时间逻辑和集合论中描述了转移系统 "图" 所描述的内容：系统可以如何行为（System(variable) 可以包含活性公式，而在使用转移系统时，活性通常以其他方式表达，例如使用 "自动机"，这只是写活性公式的图状方式）。
- 公式 Specification(variable) 描述了对系统的要求，在模型检查中通常使用时间逻辑、自动机或两者的组合来表达。（自动机是状态机的图状描述，节点的注释被解释为描述在整个无限行为中这些节点应该被访问的频率的要求）。
- 模型检查器的工作就是尝试证明上述定理。这一活动等同于推理量词时间公式是否为 TRUE，包括推理逻辑蕴含 =>。
可实现性（与合成相关的决策问题）是一个带有量词交替的公式中的量词消除。

简化来说，可实现性就是证明公式 \E system: \AA env_variable: \AA sys_variable: BehaviorOf(system, env_variable, sys_variable) => Specification(env_variable, sys_variable) 是一个定理的活动：
```
THEOREM
    \E system:
        \AA env_variable:
        \AA sys_variable:
            BehaviorOf(system, env_variable, sys_variable)
            => Specification(env_variable, sys_variable)
```
与上面形式化的验证相比，我们在这里必须推理两个不同的量词：（常量）存在量词 (\E) 和（时间）全称量词 (\AA)。在模型检查的意义上 "验证" 时，我们只需推理一种量词。

此外，在这个讨论中，"验证" 特指模型检查。如果有人说 "验证" 是指 "证明"，那么显然模型检查和控制器合成都是证明活动，在每种情况下的目标都是证明一个定理。不同之处在于定理的形式，这会影响这项活动的计算复杂性。

为了与上述关于有限状态机（"转换器"）的描述相连接：
- system 是 TLA+ 中的一个值（在集合论中设定），在时间行为中保持不变，描述设计的系统是什么样的。正是这个值由合成工具生成，即工具设计一个解决问题的系统。
  
  因此，之前提到的 "转换器" 或 "有限状态机" 对应于这个 system 值，通过操作符 BehaviorOf，如下一个项目所述。
- BehaviorOf(system, env_variable, sys_variable) 是一个公式，描述当我们部署一个由值 system 定义的系统时，世界是如何行为的。
  
  具体来说，我们所说的世界部分由变量 sys_variable 和 env_variable 表示。
  
  变量 sys_variable 被理解为描述正在设计的 "系统" 的状态，而变量 env_variable 被视为 "世界的其余部分"。
  
  更准确地说，公式 BehaviorOf(system, env_variable, sys_variable) 是逻辑和集合论中描述的图状 "状态机" 或 "转换器"，由解决合成问题的工具合成。
- 与验证的情况类似，公式 Specification(env_variable, sys_variable) 描述了所需的系统行为。
  
  在合成中，规范通常使用时间逻辑公式描述，可能与其他构造结合使用，例如图状构造（这些是时间逻辑公式的语法糖）。

关于可实现性的量词消除的描述可以在这篇论文的第四节中阅读（PDF）。

可实现性的 TLA+ 规范是 TLA+ 模块 Realizability.tla。特别是，量词交替在这里是存在的：

IsRealizable(..., ...) <=> \E f, g, mem0:  \AA x, y:  ...

符号 \E 表示常量的存在量词（在行为步骤中值保持不变的标识符）。
符号 \AA 表示变量的全称量词（在行为步骤中值可以变化的标识符）。
在 TLA+ 中，"行为" 是一个无限状态序列。（更准确地说，行为是一个将每个自然数映射到一个状态的函数；这个函数本身在 TLA+ 的元理论中）。
在 TLA+ 中，"状态" 是对名称（变量）的值的赋值。（更准确地说，状态是一个将每个变量名称映射到一个值的函数；这个函数本身在 TLA+ 的元理论中）。
变量的 "值" 是 TLA+ 元理论中的一个 "集合"，当谈到元理论中的状态时。这样的元理论值是 "值" 的语义，表示该变量在对象理论 TLA+ 中所代表的内容。

因此，这个讨论中存在两种集合论：
- TLA+ 中的集合论（对象理论是 TLA+）
- TLA+ 元理论中的集合论。
TLA+ 的元理论是定义 TLA+ 语义的地方。在 TLA+ 的元理论中，对象语言 TLA+ 的表达式以元理论的字符串形式出现（这些字符串在元理论的集合论中是 "值"，因此是元理论中的集合）。

关于 TLA+ 中可实现性的这种形式化的更多信息可以在这份文档中找到。

关于开放系统和封闭系统的正式定义可以在这篇论文中找到（PDF），其中也描述了可实现性的定义。

回答于 2025-04-18 由 Python大师

分享举报

Python：寻找模型检查工具及其转CNF的结果

1 个回答

撰写回答