问题标签 [model-checking]

• 您将模型检查用于哪些类型的应用程序？
• 你用的是什么模型检查工具？
• 您如何总结您使用该技术的经验，特别是在评估其交付更高质量软件的有效性方面？

在我的学习过程中，我有机会使用Spin，它引起了我的好奇心，即实际进行了多少模型检查以及组织从中获得了多少价值。在我的工作经验中，我从事过业务应用程序，其中（自然）没有考虑将形式验证应用于逻辑。我真的很想了解 SO 人的模型检查经验和对该主题的想法。模型检查会成为我们应该在我们的工具包中使用的更广泛使用的开发实践吗？

我试过了

但 TLC 给了我一个语法错误：

错误：TLC 在第 1 行的配置文件中发现错误。它需要 = 或 <-，但没有找到。

我也尝试将Sequences模块包含在配置文件中，但无济于事。

那么......我必须做些什么来分配一个序列？

是否有工具可以处理模型检查大型、真实世界、主要是 C++ 分布式系统，例如 KDE？

（KDE 在使用 IPC 的意义上是一个分布式系统，尽管通常所有进程都在同一台机器上。是的，顺便说一句，这是“分布式系统”的有效用法 - 检查 Wikipedia。）

该工具需要能够处理进程内事件和进程间消息。

（假设如果该工具支持 C++，但不支持 KDE 使用的其他东西，例如 moc，我们可以一起破解一些东西来解决这个问题。）

我很乐意接受不太通用的（例如，专门用于查找特定类别错误的静态分析器）或更通用的静态分析替代方案，以代替实际的模型检查器。但我只对能够实际处理 KDE 规模和复杂性项目的工具感兴趣。

有没有人接触过这个工具SPIN的模型检查，更任何模型检查的信息（并发程序）

谁能告诉我如何获取时钟变量的当前值并存储在一个整数变量中。我试过 k=t（其中 k 是整数，t 是时钟），但它会引发“不兼容的类型错误”。我也尝试过 k=(int)t，但它会引发“Unexpected T_INT”语法错误。

UPPAAL 中的时钟是否有任何类型转换可用于获取时钟的当前值并将其存储在变量中？

我正在尝试使用 Spin Model Checker 对两个对象（A 和 B）之间的游戏进行模型检查。对象在板上移动，每个位置由其 (x,y) 坐标定义。这两个物体应该不会碰撞。我有三个进程：init，A Model，B Model。我正在检查一个 ltl 属性的模型：（用于检查两个对象是否曾经占据相同位置的 liveness 属性）

我得到的错误线索是：init -> A Model -> B Model -> init

但是，根据显示的数据，我不应该得到错误线索（反例）：x_a=2，x_b=1，y_a=1，y_b=1。

同样，第一个 init 确实经过了 init 进程的所有行，但第二个只显示到它的最后一行。

此外，我的 A 模型和 B 模型仅由“do”块中的警卫和动作组成，如下所示。但是它们更复杂，并且在“->”右侧有 if 块

我需要在原子块中放入任何东西吗？我问的原因是错误跟踪显示的行甚至没有进入“do”块，它只是两个模型的第一行。

编辑： LTL 属性是错误的。我将其更改为：

但是，我仍然得到完全相同的错误线索。

我已经实现了共识算法（基于 Paxos）。我添加了一些随机测试用例，看起来不错。但是想通过模型检查进行测试？找不到正确的文章。请分享如何在 Paxos 中进行模型检查

谢谢

是否有任何用于 c# 代码的模型检查库？我正在寻找前、后条件注释类不变量，就像在 Eiffel 中一样。我用谷歌搜索了Spec#，但据我所知，它是语言扩展，而不是我期望的库。

谢谢你！

我想将边缘的防护配置为：

其中 turn 是一个时钟变量，而 me 是一个表示进程的 int。

请给我一个如何为上述谓词制作守卫的例子。

谢谢，凯文

我正在尝试使用 Alloy（对于形式逻辑也相对较新），并且尝试从完全连接的节点图开始。

从图中可以看出，节点 0 和 1 未连接。我认为我的事实足以让它完全联系起来……但也许我错过了一些东西。