Model Checking a C++ Software Framework, a Case Study
This case study shows that model checking can effectively complement traditional testing for software frameworks, offering new insights and defect detection, though it is incremental in applying existing tools to a specific domain.
The paper applied SPIN and DIVINE model checkers to verify the ADAPRO C++ framework, finding design flaws with SPIN and defects in heavily tested code with DIVINE, demonstrating that model checking is feasible and valuable for library-level development.
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.