model-checking - 自旋 - 形式验证

Question

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

Answer 1

是的，SPIN 是一个非常好的模型检查器，但我想知道你想要什么？您只是想听听，是的，我已经听过并玩过 SPIN，还是想要关于如何对源代码进行模型检查的建议？

例如，如果您是一名 C 程序员，请使用ESBMC，编写一个小程序并在其上运行 ESBMC。

这应该让您开始了解可以做什么以及如何去做。顺便说一句，对于初学者来说，模型检查不是静态分析。它实际上要强大得多。这是防静电分析。模型检查实际上“在（非常狭窄的）意义上”模拟您的程序并找到它实际上会失败的情况（参数组合、异常情况、边界情况）。