一句话：通过 Spin 与 Divine 对 CERN 的 C++ 框架 ADAPRO 进行模型检测，发现设计及经大量测试的代码缺陷。
本文报告将模型检测用于 C++ 框架 ADAPRO 的案例研究。ADAPRO 最初由 CERN 开发；作者用 Spin 在设计层建模验证，用 Divine 验证与实现交互的简单测试应用。两类模型检测器各有优缺点，但互补使用带来了传统测试与分析难以获得的洞见：将 C++ 源码翻译为 Spin 模型有助于发现原始设计缺陷，Divine 则在已历经数百小时单元、集成与验收测试的代码中发现缺陷。作者认为模型检测易于集成到项目工作流，不仅可验证，也可用于确认，对库级代码开发现实且值得。
This paper presents a case study on applying two model checkers, Spin and Divine, to verify key properties of a C++ software framework, known as ADAPRO, originally developed at CERN. Spin was used for verifying properties on the design level. Divine was used for verifying simple test applications that interacted with the implementation. Both model checkers were found to have their own respective sets of pros and cons, but the overall experience was positive. Because both model checkers were used in a complementary manner, they provided valuable new insights into the framework, which would arguably have been hard to gain by traditional testing and analysis tools only. Translating the C++ source code into the modeling language of the Spin model checker helped to find flaws in the original design. With Divine, defects were found in parts of the code base that had already been subject to hundreds of hours of unit tests, integration tests, and acceptance tests. Most importantly, model checking was found to be easy to integrate into the workflow of the software project and bring added value, not only as verification, but also validation methodology. Therefore, using model checking for developing library-level code seems realistic and worth the effort.