# Model Checking a C++ Software Framework, a Case Study

## TL;DR

This case study demonstrates how applying two model checkers, SPIN and DIVINE, to a CERN-developed C++ framework can uncover design flaws and defects, providing valuable insights beyond traditional testing methods.

## Contribution

The paper shows the practical application and benefits of using two complementary model checkers for verifying a complex C++ software framework at CERN.

## Key findings

- Model checking revealed design flaws in the framework.
- DIVINE identified defects in thoroughly tested code.
- Model checking was easily integrated into the development workflow.

## Abstract

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.