问题标签 [model-checking]

是否有一种算法来检查彩色 Petri 网的边界标准（意味着状态空间是有限的）（或者这个属性是不可判定的）？

给定一个系统及其完整的状态空间，我可以说该状态空间是该系统行为的正式规范吗？

我正在尝试使用DDcal来评估二元决策图。当我尝试评估某些公式时，例如：a+b*c'，我总是得到这个错误：

有谁知道我该如何解决这个错误？

感谢您的任何见解。

我们使用 Z3 进行有界模型检查。为此，我们提供了一大堆如下形式的表达式：

换句话说，我们通过为每个时间步提供单独的表达式来编码时间（步）的流逝。显然，这会导致数千个表达式。

虽然 Z3 解决这些问题所花费的时间是可以接受的（考虑到我们拥有的状态机的复杂性），但通过 Z3 JNI Java API 构建所有这些表达式需要相当长的时间（几秒钟）。

所以这是我的问题：有没有更简单的方法来告诉 Z3 通过一些专门的 API 创建所有这些时间展开的表达式？

我正在用 B 方法编写系统的一些规范。我有以下变量，它们是一般集合的子集：

1. 第一个符号：a :={x,y,z,v} b :={x,y,z}

我想声明一个规则，只要集合“b”中存在某些东西，它也存在于集合“a”中，这有助于将上述规范编写如下：

2. 第二种表示法：a :={v} b :={x,y,z}

第二个符号的解释：我希望机器从 a :={v}、b :={x,y,z} 和规则中推断出 a :={x,y,z,v}。

我怎样才能表达规则，所以我避免第一个符号，而是写第二个符号？

我尝试了以下但没有奏效

目前我正在尝试将系统原型转换为过渡系统模型。我有一些 LTL 属性，我想使用模型检查工具 NuSMV 验证这些属性。我只是介绍如何通过定义原子属性和其他数学方面来开始建模。

模型的图示

如何在 PROMELA 中将 LTL 转换为 Automata？我知道使用命令 SPIN -f "ltl x" 可以将 LTL 转换为从不声明，但我想要 LTL 的自动机而不是否定的自动机。如果我之前否定 LTL 以生成从不声明，这是正确的。谁能帮我？

符号执行和模型检查（例如在模型转换中）有什么区别？我不明白他们的区别。他们是一样的吗？！

在像 CBMC（C 的有界模型检查器）这样的模型检查器中，用户定义的断言语句采用布尔条件，模型检查器检查程序所有可能执行的条件是真还是假。

在 C 编程中，我们使用头文件 assert.h 定义 assert() 宏。如果它的参数评估为 TRUE，则 assert() 宏返回 TRUE，如果评估为 FALSE，则执行某种操作。许多编译器会在失败的 assert() 上中止程序。

有人可以澄清模型检查和编程世界中这两个断言之间的区别吗？

是否可以使用 Spin 获得多个（或全部）违规跟踪？

例如，我在下面创建了 Promela 模型：

它有一个简单的互斥锁实现。可以预期进程 A 和 B 不会一起到达它们的临界区，我编写了一个 LTL 表达式来检查这一点。

跑步

表明该属性无效且正在运行

显示违反该属性的语句序列。

这表明语句序列（由标签指示）'B1' -> 'A1' -> 'B2' -> 'A2' 违反了该属性，但还有其他交错选项导致该属性（例如 'A1' -> ' B1'->'B2'->'A2'）。

我可以要求 Spin 给我多条（或全部）痕迹吗？