1

我想用模型检查器测试我的代码，并以自动化的方式制作一个 FSM。为此，我需要一个模型检查器并将 FSM 结果转换为 CNF。

有什么建议我可以在 Python 中做到这一点吗？我只知道 CBMC，但仅限于 C。

谢谢阿德里安

4

1 回答 1

6

Python不是一种适合模型检查的语言，例如鸭子类型可以很自由地引发异常。如果您的 Python代码本质上是procedural，那么您可以尝试先将其转换为Cusingpy2c或其他等效代码。

然后用于从代码modex中提取Promela模型。C最后一步称为抽象。然后您可以使用SPIN模型检查器来验证感兴趣的属性。

如果 CNF 代表“ Conjunctive Normal Form ”，那么我不明白 CNF 与模型检查结果的关系。模型检查产生：

  • “是的，您的模型模拟了您提供的逻辑公式”或

  • “不，它没有，这是一个反例为什么不”。

CNF 是布尔公式的一种特殊句法形式。

如果您提到 CNF 与有界模型检查CBMC和其中涉及的SAT求解相关，那么请注意SPIN接受使用 Promela 语言表达的 Kripke 模型作为输入。因此，您无需将任何内容转换为布尔公式，此外您还可以运行完整的活性验证检查。

此工具列表包括模型检查器。特别是，如果您想编写一个从 Python 到 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的演化variable，那么公式Specification(variable)也是TRUE的演化variable。

    在有限过渡系统和模型检查方面与上述描述联系起来：

    • 该公式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)是一个公式，描述了当我们部署由 value 定义的系统时世界的行为方式system。

      具体来说，我们所说的世界的一部分由变量sys_variable,表示env_variable。

      变量sys_variable被理解为描述正在设计的“系统”的状态，变量env_variable被认为是“世界的其余部分”。

      更准确地说，该公式BehaviorOf(system, env_variable, sys_variable)是由解决合成问题的工具合成的类似图形的“状态机”或“转换器”的逻辑和集合论描述。

    • 与验证的情况类似，该公式Specification(env_variable, sys_variable)描述了所需的系统行为。

      在综合中，规范通常使用时间逻辑公式来描述，可能与其他构造结合，例如类似图形的构造（它们是时间逻辑公式的句法糖）。

可以在本文的第 IV 部分( 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 ) 中找到开放系统和封闭系统的正式定义，该文件还描述了可实现性的定义。

于 2014-09-13T06:43:58.260 回答