旋转 - 形式验证

Question

有没有人接触过这个工具SPIN的模型检查,更多的模型检查信息(并发程序)

Answer 1

是的,SPIN是一个非常好的模型检查器,但我想知道你想要什么？你只是想听到是的,我听过并玩过SPIN,或者你想要建议如何建模检查源代码？

例如,如果您是C程序员,请亲自参与ESBMC,编写一个小程序并在其上运行ESBMC.

这应该让你开始了解可以做什么以及如何做.顺便说一句,对于初学者,模型检查不是静态分析.它实际上更强大.这是抗静电分析.模型检查实际上"在(非常狭窄的)意义上"模拟您的程序并找到实际失败的情况(参数组合,异常情况,边界情况).