有人接触过用这个工具进行模型检查SPIN ，甚至更多model checking的任何信息(并发程序)
最佳答案
是的，SPIN 是一个非常好的模型检查器，但我想知道你想要什么？您只是想听听，是的，我已经听过并玩过 SPIN，还是您想要有关如何建模检查源代码的建议？
例如，如果您是 C 程序员，请输入 ESBMC ，编写一个小程序并在其上运行 ESBMC。
这应该让您开始了解可以做什么以及如何做。顺便说一句，对于初学者来说，模型检查不是静态分析。它实际上更强大。这是抗静电分析。模型检查实际上“在(非常狭隘的)意义上”模拟您的程序并找到它实际上会失败的情况(参数组合、异常情况、边界情况)。
关于model-checking - Spin - 形式验证，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/6038349/