What types of applications have you used model checking for?
We used the Java Path Finder model checker to verify some security (deadlock, race condition) and temporal properties (using Linear temporal logic to specify them). It supports classical assertions (like NotNull) on Java (bytecode) - it is for program model checking.
What model checking tool did you use?
We used Java Path Finder (for academic purposes). It's open source software developed by NASA initially.
How would you summarize your experience w/ the technique, specifically in evaluating its effectiveness in delivering higher quality software?
Program model checking has a major problem with state space explosion (memory & disk usage). But there are a wide variety of techniques to reduce the problems, to handle large artifacts, such as partial order reduction, abstraction, symmetry reduction, etc.
We have used several model checkers in teaching, systems design, and systems development. Our toolbox includes SPIN, UPPAL, Java Pathfinder, PVS, and Bogor. Each has its strengths and weaknesses. All find problems with models that are simply impossible for human beings to discover. Their usability varies, though most are pushbutton automated.
When to use a model checker? I'd say any time you are describing a model that must have (or not have) particular properties and it is any larger than a handful of concepts. Anyone who thinks that they can describe and understand anything larger or more complex is fooling themselves.
We used a virtual machine to walk each and every possible path/state of the program, using A* and some heuristic, depending on the kind of error (deadlock, I/O errors, ...)
It was inspired by Java Pathfinder and it worked with C++ code. (Everything GCC could compile)
But in our experiences this kind of technology will not be used in business applications soon, because of GUI related problems, the work necessary for creating an initial test environment and the enormous hardware requirements. (You need lots of RAM and disc space, because of the gigantic state space)
顺便问一下，有《SPIN for Dummies》一书吗？ 我必须从“The SPIN Model Checker”一书和各种在线教程中学习它。
I used SPIN to find a concurrency issue in PLC software. It found an unsuspected race condition that would have been very tough to find by inspection or testing.
By the way, is there a "SPIN for Dummies" book? I had to learn it out of "The SPIN Model Checker" book and various on-line tutorials.
虽然这些工具使用起来很有趣，但我认为当您将它们与动态地对程序施加约束的东西结合起来时，它们确实会发光（这样就更容易验证程序的“有用”东西）。 我们最终采用了 Spring WebFlow 框架，它使用 XML 编写一个类似状态机的文件，该文件指定哪些网页可以转换到哪些其他网页，并使用 SMV 能够对所述应用程序执行验证 (这里是无耻的插件）。
I just finished a class on model checking and the big tools we used were Spin and SMV. We ended up using them to check properties on common synchronization problems, and I found SMV just a little bit easier to use.
Although these tools were fun to use, I think they really shine when you combine them with something that dynamically enforces constraints on your program (so that it's a bit easier to verify 'useful' things about your program). We ended up taking the Spring WebFlow framework, which uses XML to write a state-machine like file that specifies which web pages can transition to which other ones, and using SMV to be able to perform verification on said applications (shameless plug here).
To answer your last question, I think model checking is definitely useful to have, but I lean more towards using unit testing as a technique that makes me feel comfortable about delivering my final product.
发布评论
评论（5）
我们使用 Java Path Finder 模型检查器来验证一些安全性（死锁、竞争条件）和时间属性（使用线性时间逻辑来指定它们）。 它支持 Java（字节码）上的经典断言（如 NotNull）——用于程序模型检查。
我们使用 Java Path Finder（用于学术目的）。 它最初是由 NASA 开发的开源软件。
程序模型检查的一个主要问题是状态空间爆炸（内存和磁盘使用）。 但是有各种各样的技术可以减少问题、处理大型工件，例如偏序约简、抽象、对称性约简等。
We used the Java Path Finder model checker to verify some security (deadlock, race condition) and temporal properties (using Linear temporal logic to specify them). It supports classical assertions (like NotNull) on Java (bytecode) - it is for program model checking.
We used Java Path Finder (for academic purposes). It's open source software developed by NASA initially.
Program model checking has a major problem with state space explosion (memory & disk usage). But there are a wide variety of techniques to reduce the problems, to handle large artifacts, such as partial order reduction, abstraction, symmetry reduction, etc.
我们在教学、系统设计和系统开发中使用了多种模型检查器。 我们的工具箱包括 SPIN、UPPAL、Java Pathfinder、PVS 和 Bogor。 每个都有其优点和缺点。 所有人都发现模型存在人类根本无法发现的问题。 它们的可用性各不相同，但大多数都是按钮自动化的。
何时使用模型检查器？ 我想说的是，任何时候你描述的模型必须具有（或不具有）特定的属性，并且它比几个概念要大。 任何认为自己可以描述和理解更大或更复杂事物的人都是在自欺欺人。
We have used several model checkers in teaching, systems design, and systems development. Our toolbox includes SPIN, UPPAL, Java Pathfinder, PVS, and Bogor. Each has its strengths and weaknesses. All find problems with models that are simply impossible for human beings to discover. Their usability varies, though most are pushbutton automated.
When to use a model checker? I'd say any time you are describing a model that must have (or not have) particular properties and it is any larger than a handful of concepts. Anyone who thinks that they can describe and understand anything larger or more complex is fooling themselves.
我在大学期间对此主题进行了一些研究，扩展了状态探索装配模型检查器。
我们使用虚拟机来遍历程序的每一个可能的路径/状态，使用 A* 和一些启发式方法，具体取决于错误的类型（死锁、I/O 错误等）。
它的灵感来自 Java Pathfinder 它适用于 C++ 代码。 （GCC 可以编译的所有内容）
但根据我们的经验，这种技术不会很快用于商业应用程序，因为 GUI 相关问题、创建初始测试环境所需的工作以及巨大的硬件要求。 （由于状态空间巨大，您需要大量 RAM 和磁盘空间）
I've done some research on that subject during my time at the university, expanding the State Exploring Assembly Model Checker.
We used a virtual machine to walk each and every possible path/state of the program, using A* and some heuristic, depending on the kind of error (deadlock, I/O errors, ...)
It was inspired by Java Pathfinder and it worked with C++ code. (Everything GCC could compile)
But in our experiences this kind of technology will not be used in business applications soon, because of GUI related problems, the work necessary for creating an initial test environment and the enormous hardware requirements. (You need lots of RAM and disc space, because of the gigantic state space)
我使用 SPIN 发现 PLC 软件中的并发问题。 它发现了一个意想不到的竞争条件，而通过检查或测试很难发现这种竞争条件。
顺便问一下，有《SPIN for Dummies》一书吗？ 我必须从“The SPIN Model Checker”一书和各种在线教程中学习它。
I used SPIN to find a concurrency issue in PLC software. It found an unsuspected race condition that would have been very tough to find by inspection or testing.
By the way, is there a "SPIN for Dummies" book? I had to learn it out of "The SPIN Model Checker" book and various on-line tutorials.
我刚刚完成了模型检查课程，我们使用的主要工具是 Spin 和 SMV。 我们最终使用它们来检查常见同步问题的属性，我发现 SMV 更容易使用。
虽然这些工具使用起来很有趣，但我认为当您将它们与动态地对程序施加约束的东西结合起来时，它们确实会发光（这样就更容易验证程序的“有用”东西）。 我们最终采用了 Spring WebFlow 框架，它使用 XML 编写一个类似状态机的文件，该文件指定哪些网页可以转换到哪些其他网页，并使用 SMV 能够对所述应用程序执行验证 (这里是无耻的插件）。
为了回答你的最后一个问题，我认为模型检查绝对有用，但我更倾向于使用单元测试作为一种技术，让我对交付最终产品感到放心。
I just finished a class on model checking and the big tools we used were Spin and SMV. We ended up using them to check properties on common synchronization problems, and I found SMV just a little bit easier to use.
Although these tools were fun to use, I think they really shine when you combine them with something that dynamically enforces constraints on your program (so that it's a bit easier to verify 'useful' things about your program). We ended up taking the Spring WebFlow framework, which uses XML to write a state-machine like file that specifies which web pages can transition to which other ones, and using SMV to be able to perform verification on said applications (shameless plug here).
To answer your last question, I think model checking is definitely useful to have, but I lean more towards using unit testing as a technique that makes me feel comfortable about delivering my final product.