您对软件模型检查的体验是什么？

Question

• 您使用了哪些类型的应用程序进行模型检查？
• 你使用什么模型检查工具？
• 您如何总结您使用该技术的经验,特别是在评估其提供更高质量软件的有效性方面？

在我学习的过程中,我有机会使用Spin,它引起了我对实际模型检查进行了多少以及组织从中获取多少价值的好奇心.在我的工作经历中,我从事过业务应用程序,其中(自然)没有考虑将正式验证应用于逻辑.我真的很想了解SO人员的模型检查经验和关于这个主题的想法.模型检查是否会成为我们工具箱中应该使用的更广泛使用的开发实践？

Answer 1

我刚刚完成了一门关于模型检查的课程，我们使用的主要工具是Spin和SMV。我们最终使用它们来检查常见同步问题的属性，我发现 SMV 更容易使用。

虽然这些工具使用起来很有趣，但我认为当您将它们与动态地对程序施加约束的东西结合起来时，它们确实会发光（这样就更容易验证程序的“有用”东西）。我们最终采用了Spring WebFlow 框架，它使用 XML 编写一个类似状态机的文件，指定哪些网页可以转换到其他网页，并使用 SMV 能够对所述应用程序执行验证（这里是无耻的插件）。

为了回答你的最后一个问题，我认为模型检查绝对有用，但我更倾向于使用单元测试作为一种技术，让我对交付最终产品感到放心。