在我的学习过程中，我有机会使用Spin，它引起了我的好奇心，对实际模型检查进行了多少以及组织从中获得了多少价值感到好奇。在我的工作经验中，我从事过业务应用程序，其中（自然）没有考虑将形式验证应用于逻辑。我真的很想了解 SO 人的模型检查经验和对该主题的想法。模型检查是否会成为我们应该在我们的工具包中使用的更广泛使用的开发实践？
【问题讨论】：
标签： algorithm correctness formal-methods formal-verification model-checking
我刚刚完成了关于模型检查的课程，我们使用的大工具是 Spin 和 SMV。我们最终使用它们来检查常见同步问题的属性，我发现 SMV 更易于使用。
虽然这些工具使用起来很有趣，但我认为当您将它们与动态强制程序约束的东西结合使用时，它们真的会大放异彩（这样更容易验证程序的“有用”事物）。我们最终采用了Spring WebFlow framework，它使用 XML 编写一个类似状态机的文件，指定哪些网页可以转换到其他网页，并使用 SMV 能够对所述应用程序执行验证 (shameless plug here)。
为了回答你的最后一个问题，我认为模型检查绝对有用，但我更倾向于使用单元测试作为一种让我对交付最终产品感到自在的技术。
【讨论】：
我们在教学、系统设计和系统开发中使用了多个模型检查器。我们的工具箱包括 SPIN、UPPAL、Java Pathfinder、PVS 和 Bogor。每个都有其优点和缺点。所有人都发现了人类根本无法发现的模型问题。它们的可用性各不相同，但大多数都是按钮自动化的。
何时使用模型检查器？我会说，任何时候您描述的模型都必须具有（或不具有）特定属性，并且它比少数概念大。任何认为自己可以描述和理解更大或更复杂事物的人都是在自欺欺人。
【讨论】：
您将模型检查用于哪些类型的应用程序？
我们使用 Java Path Finder 模型检查器来验证一些安全性（死锁、竞争条件）和时间属性（使用线性时间逻辑来指定它们）。它支持 Java（字节码）上的经典断言（如 NotNull）——用于程序模型检查。
你用的是什么模型检查工具？
我们使用了Java Path Finder（用于学术目的）。它是最初由 NASA 开发的开源软件。
您如何总结您使用该技术的经验，特别是在评估其在交付更高质量软件方面的有效性方面？
程序模型检查存在状态空间爆炸（内存和磁盘使用）的主要问题。但是有各种各样的技术可以减少问题，处理大型工件，例如偏序减少、抽象、对称减少等。
【讨论】：
我使用 SPIN 来查找 PLC 软件中的并发问题。它发现了一个通过检查或测试很难发现的未预料到的竞争条件。
顺便问一下，有没有“SPIN for Dummies”一书？我必须从“The SPIN Model Checker”一书和各种在线教程中学习它。
【讨论】：
我在大学期间对该主题进行了一些研究，扩展了State Exploring Assembly Model Checker。
我们使用虚拟机来遍历程序的每一个可能的路径/状态，使用 A* 和一些启发式方法，具体取决于错误的类型（死锁、I/O 错误……）
它的灵感来自Java Pathfinder，它使用 C++ 代码工作。 （GCC 可以编译的所有东西）
但根据我们的经验，这种技术不会很快用于商业应用程序，因为 GUI 相关问题、创建初始测试环境所需的工作以及巨大的硬件需求。 （由于状态空间巨大，您需要大量 RAM 和磁盘空间）
【讨论】：