简单的模型检查工具

有一个简单的模型检查工具.我计划实现一个模型检查工具,它将分析一些预定义属性的代码.

一个重要的工具是SPIN,使用Promela语言.如果您使用LaTeX,还有TLA +.

这些不会分析您的代码,但会让您为您的假设和状态转换表达模型,然后分析无效状态.换句话说,它们将检测模型中的问题,而不是模型的实现.

我看过Goanna的演示,但我不知道它是否可用(商业或其他); 这具有实际分析源代码的优势.

只是再看一下你的问题和你问题中的评论,听起来你真的应该首先阅读一些文献.也许,旋转模型检查器或指定系统 (可从Leslie Lamport的网站下载).您需要重新构建问题,这样才不会尝试解决暂停问题.