• 我们对模型检查使用了哪些类型的应用程序？
• 我们使用了哪种模型检查工具？
• 我们如何总结使用该技术的经验，尤其是评估其在交付更高质量软件方面的有效性？

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

解决方案

回答

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

尽管这些工具使用起来很有趣，但我认为将它们与动态地对程序施加约束的某些东西结合使用时，它们确实会发光(这样可以更容易地验证有关程序的"有用"内容)。我们最终采用了Spring WebFlow框架，该框架使用XML编写类似于状态机的文件，该文件指定哪些网页可以转换到其他网页，并使用SMV能够对所述应用程序执行验证(此处是无耻的插件)。

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

回答

我使用SPIN在PLC软件中发现并发问题。它发现了意外的比赛条件，通过检查或者测试很难找到。

顺便说一句，有一本书"傻瓜的傻瓜"吗？我必须从" The SPIN Model Checker"这本书和各种在线教程中学习。

回答

在大学期间，我已经对该主题进行了一些研究，扩展了"状态探索装配体模型检查器"(State Exploring Assembly Model Checker)。

根据错误的类型(死锁，I / O错误，...)，我们使用虚拟机使用A *和一些启发式方法遍历程序的每个可能路径/状态。

它受到Java Pathfinder的启发，并与C ++代码一起使用。 (所有GCC都可以编译)

但是，根据我们的经验，由于与GUI相关的问题，创建初始测试环境所需的工作以及巨大的硬件要求，这种技术不会很快用于业务应用程序。 (由于巨大的状态空间，我们需要大量的RAM和磁盘空间)

回答

我们在教学，系统设计和系统开发中使用了几种模型检查器。我们的工具箱包括SPIN，UPPAL，Java Pathfinder，PVS和Bogor。每个都有其优点和缺点。所有人都发现了人类根本无法发现的模型问题。它们的可用性各不相同，尽管大多数按钮是自动化的。

何时使用模型检查器？我想说的是，只要我们描述的模型必须具有(或者不具有)特定的属性，并且它比少数几个概念都要大。任何认为自己可以描述和理解更大或者更复杂的事物的人都在自欺欺人。