pith. sign in

arxiv: 1907.00172 · v1 · pith:ZBIMW4EWnew · submitted 2019-06-29 · 💻 cs.SE

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

John L{\aa}ng , I.S.W.B. Prasetya This is my paper

Pith reviewed 2026-05-25 13:10 UTC · model grok-4.3

classification 💻 cs.SE
keywords model checkingSPINDIVINEC++ frameworksoftware verificationcase studyADAPROCERN
0
0 comments X

The pith

Model checking with SPIN and DIVINE on a C++ framework uncovers design flaws and code defects missed by extensive testing while integrating easily into the development workflow.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper reports a case study applying two model checkers to the ADAPRO C++ software framework from CERN. SPIN was applied at the design level by translating source code into its modeling language, while DIVINE was used to check simple test applications against the actual implementation. The two tools complemented each other and surfaced issues in the design as well as defects in code that had already received hundreds of hours of unit, integration, and acceptance tests. The authors found the approach straightforward to fit into an existing project workflow and concluded that model checking is realistic and worthwhile for library-level C++ code. A sympathetic reader would care because the work suggests a practical route to greater reliability in complex library software where traditional testing alone may leave gaps.

Core claim

The authors applied SPIN to verify properties on the design level of the ADAPRO framework and DIVINE to verify simple test applications interacting with the implementation. Translation of the C++ source into SPIN's modeling language exposed flaws in the original design. DIVINE located defects in sections of the code base already covered by hundreds of hours of testing. The complementary use of both checkers delivered new insights that would have been difficult to obtain with traditional testing and analysis tools alone. Model checking integrated smoothly into the project workflow and added value both as verification and as validation methodology.

What carries the argument

Complementary application of SPIN for design-level verification via source translation and DIVINE for implementation-level verification on test applications interacting with the C++ code of the ADAPRO framework.

If this is right

  • Translating C++ source code into SPIN's modeling language can expose flaws present in the original design.
  • DIVINE can detect defects in parts of the code base already subjected to hundreds of hours of unit, integration, and acceptance tests.
  • The two model checkers can be used in a complementary manner to generate insights that traditional testing and analysis tools are unlikely to produce.
  • Model checking can serve as both a verification and a validation methodology.
  • Model checking can be integrated into the workflow of a software project developing library-level code without major obstacles.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Other C++ libraries handling concurrency or complex state might see similar gains from early use of these model checkers.
  • Teams working on high-reliability libraries could shift some effort from prolonged testing campaigns toward model checking.
  • The case study supplies a concrete template that other projects could adapt to evaluate model checking for their own code bases.
  • Wider adoption would benefit from additional case studies on frameworks with different architectural styles.

Load-bearing premise

The positive experience, complementary insights, and feasibility conclusions from the ADAPRO case study generalize to other C++ library projects and development workflows.

What would settle it

A separate C++ library project in which applying SPIN and DIVINE produces no new insights beyond what traditional testing already found and cannot be integrated into the workflow without major disruption or extra effort.

Figures

Figures reproduced from arXiv: 1907.00172 by I.S.W.B. Prasetya, John L{\aa}ng.

Figure 1
Figure 1. Figure 1: Thread state transition diagram instances. The role of the framework is to manage Threads [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: Session initialization and user-defined worker factories. Supervisor then takes care of constructing the workers by applying the factories to the logger and configuration [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Command propagation 4.1 Preconditions The ADAPRO framework relies on a programming contract be￾tween the framework developers and the application developers. There are necessary preconditions/assumptions on the environment and user-defined code, that ADAPRO has to take as granted. The full list of preconditions is given below for completeness: (1) There will be no sabotage or force majeur incidents of any … view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents a case study on applying the model checkers SPIN (at the design level via translation to Promela) and DIVINE (on test applications interacting with the C++ implementation) to the ADAPRO framework developed at CERN. It reports that SPIN translation revealed design flaws and that DIVINE identified defects in code subjected to hundreds of hours of unit, integration, and acceptance tests. The authors conclude that the complementary use of the tools yielded insights difficult to obtain via traditional methods, that model checking integrates easily into the workflow, and that its use for library-level C++ code therefore seems realistic and worth the effort.

Significance. If the reported findings hold, the work supplies a concrete, positive example of model-checking integration into an industrial C++ library project, illustrating complementary strengths of two tools and potential added value beyond testing. The explicit mention of workflow integration is a practical strength. However, the single-framework scope and absence of effort metrics or replication limit the force of the generalization to other C++ library projects.

major comments (2)
  1. [Abstract] Abstract: the central claim that 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' is load-bearing for the assertion that model checking supplies insights 'arguably hard to gain by traditional testing,' yet the manuscript supplies no description of the properties checked, the modeling of C++ constructs in DIVINE, or any independent confirmation that the reported defects were genuine rather than tool artifacts.
  2. [Conclusion] The feasibility conclusion that 'using model checking for developing library-level code seems realistic and worth the effort' extrapolates from the single ADAPRO experience; no comparative effort data, success/failure rates on other C++ projects, or replication study is provided to support the generalization beyond this CERN framework.
minor comments (1)
  1. [Abstract] The abstract and body repeatedly use 'arguably' and 'seems' when stating the main conclusion; a more precise statement of the scope of the claim would improve clarity.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the constructive comments on our case study. We address each major point below and indicate planned revisions.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that 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' is load-bearing for the assertion that model checking supplies insights 'arguably hard to gain by traditional testing,' yet the manuscript supplies no description of the properties checked, the modeling of C++ constructs in DIVINE, or any independent confirmation that the reported defects were genuine rather than tool artifacts.

    Authors: The manuscript body contains sections detailing the properties verified with DIVINE and the test applications used, along with how C++ code was exercised. However, we agree that the abstract claim would be better supported by expanded description. We will revise to include explicit summaries of the checked properties, the relevant C++ modeling aspects in DIVINE, and confirmation steps taken with the ADAPRO developers to validate the defects. revision: yes

  2. Referee: [Conclusion] The feasibility conclusion that 'using model checking for developing library-level code seems realistic and worth the effort' extrapolates from the single ADAPRO experience; no comparative effort data, success/failure rates on other C++ projects, or replication study is provided to support the generalization beyond this CERN framework.

    Authors: We agree the paper reports a single-framework case study and therefore cannot supply comparative metrics or replication results from additional projects. We will revise the conclusion to frame the feasibility statement explicitly as an observation from the ADAPRO experience, highlight the single-case limitation, and present the outcome as suggestive rather than a broad generalization. revision: yes

standing simulated objections not resolved
  • Supplying effort metrics, success rates, or replication results from other C++ library projects, as the study is confined to the single ADAPRO framework.

Circularity Check

0 steps flagged

No circularity: observational case study with no derivations or self-referential reductions

full rationale

The paper is a pure case study report on applying SPIN and DIVINE to one C++ framework (ADAPRO). It contains no equations, parameters, predictions, or first-principles derivations. All claims rest on direct observation of tool outputs versus existing tests on this single codebase. No self-citation load-bearing steps, fitted inputs renamed as predictions, or ansatzes appear. The generalization to 'library-level code' is an informal opinion, not a constructed equivalence. Per rules, this is self-contained against external benchmarks and receives the default non-finding.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is an empirical case-study paper with no mathematical content.

pith-pipeline@v0.9.0 · 5744 in / 988 out tokens · 31455 ms · 2026-05-25T13:10:32.893335+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages · 1 internal anchor

  1. [1]

    González Suárez

    Borja Fernández Adiego, Dániel Darvas, Jean-Charles To urnier, En- rique Blanco Viñuela, and Víctor M. González Suárez. 2014. B ringing Automated Model Checking to PLC Program Development — A CERN Case Study —. IFAC Proceedings Volumes 47, 2 (2014), 394 – 399. DOI: http://dx.doi.org/https://doi.org/10.3182/20140514-3-FR-4046.00051 12th IFAC International ...

    work page doi:10.3182/20140514-3-fr-4046.00051 2014

  2. [2]

    Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking . MIT Press

    work page 2008

  3. [3]

    Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeá š Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill. 2017. Model Che cking of C and C++ with DIVINE 4. In Automated Technology for Verification and Analysis (ATV A

    work page 2017

  4. [4]

    (LNCS), Vol. 10482. Springer, 201–207

    work page

  5. [5]

    Mordechai Ben-Ari. 2008. Principles of the Spin Model Checker . Springer. DOI: http://dx.doi.org/10.1007/978-1-84628-770-1

    work page doi:10.1007/978-1-84628-770-1 2008

  6. [6]

    Chandra, P

    S. Chandra, P. Godefroid, and C. Palm. 2002. Software mod el checking in prac- tice: an industrial case study. In Proceedings of the 24th International Conference on Software Engineering. ICSE 2002 . 431–441

    work page 2002

  7. [7]

    Zhe Chen, Yi Gu, Zhiqiu Huang, Jun Zheng, Chang Liu, and Zi yi Liu. 2015. Model checking aircraft controller software: a case study. Software: Practice and Experience 45, 7 (2015), 989–1017. DOI:http://dx.doi.org/10.1002/spe.2242 arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1002/spe.2242

    work page doi:10.1002/spe.2242 2015

  8. [8]

    Cimatti, E

    A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M . Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. NuSMV Version 2: An Open Source Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CA V 2002) (LNCS), Vol. 2404. Springer, Copenhagen, Denmark

    work page 2002

  9. [9]

    de la Cámara, M

    P. de la Cámara, M. M. Gallardo, P. Merino, and D. Sanán. 20 05. Model Checking Software with Well-defined APIs: The Socket Case. I n Proceed- ings of the 10th International Workshop on Formal Methods fo r Industrial Critical Systems (FMICS ’05) . ACM, New York, NY, USA, 17–26. DOI: http://dx.doi.org/10.1145/1081180.1081184

    work page doi:10.1145/1081180.1081184

  10. [10]

    B Abelev et al and. 2014. Upgrade of the ALICE Experiment: Letter Of Intent. Journal of Physics G: Nuclear and Particle Physics 41, 8 (jul 2014), 087001. DOI: http://dx.doi.org/10.1088/0954-3899/41/8/087001

    work page doi:10.1088/0954-3899/41/8/087001 2014

  11. [11]

    John Fitzgerald, Juan Bicarregui, Peter Gorm Larsen, a nd Jim Wood- cock. 2013. Industrial Deployment of Formal Methods: Trends and Chal- lenges. Springer Berlin Heidelberg, Berlin, Heidelberg, 123–143 . DOI: http://dx.doi.org/10.1007/978-3-642-33170-1_10

    work page doi:10.1007/978-3-642-33170-1_10 2013

  12. [12]

    Franek and C

    B. Franek and C. Gaspar. 2004. SMI++ object oriented fra mework for de- signing and implementing distributed control systems. In IEEE Symposium Conference Record Nuclear Science 2004. , Vol. 3. 1831–1835 Vol. 3. DOI: http://dx.doi.org/10.1109/NSSMIC.2004.1462600

    work page doi:10.1109/nssmic.2004.1462600 2004

  13. [13]

    Xiang Gan, Jori Dubrovin, and Keijo Heljanko. 2014. A sy m- bolic model checking approach to verifying satellite onboa rd soft- ware. Science of Computer Programming 82 (2014), 44 – 55. DOI: http://dx.doi.org/https://doi.org/10.1016/j.scico.2013.03.005 Special Issue on Automated Verification of Critical Systems (A VoCS’11)

    work page doi:10.1016/j.scico.2013.03.005 2014

  14. [14]

    Gaspar, M

    C. Gaspar, M. Dönszelmann, and Ph. Charpentier. 2001. D IM, a portable, light weight package for information publishing, data transfer and inter-process com- munication. Computer Physics Communications 140, 1 (2001), 102 – 109. DOI: http://dx.doi.org/https://doi.org/10.1016/S0010-4655(01)00260-0 CHEP2000

    work page doi:10.1016/s0010-4655(01)00260-0 2001

  15. [15]

    Holzmann

    Gerard J. Holzmann. 1997. The model checker SPIN. IEEE Trans- actions on Software Engineering 23, 5 (May 1997), 279–295. DOI: http://dx.doi.org/10.1109/32.588521

    work page doi:10.1109/32.588521 1997

  16. [16]

    Holzmann

    Gerard J. Holzmann. 2001. Economics of Software Verific ation. In Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE ’01) . ACM, New York, NY, USA, 80–89. DOI: http://dx.doi.org/10.1145/379605.379681

    work page doi:10.1145/379605.379681 2001

  17. [17]

    Holzmann, R

    Gerard J. Holzmann, R. Joshi, and A. Groce. 2008. Swarm V erification. In 2008 23rd IEEE/ACM International Conference on Automated Software Engineering. 1–6. DOI:http://dx.doi.org/10.1109/ASE.2008.9

    work page doi:10.1109/ase.2008.9 2008

  18. [18]

    Holzmann and M

    Gerard J. Holzmann and M. H. Smith. 1999. A practical met hod for ver- ifying event-driven software. In Proceedings of the 1999 International Con- ference on Software Engineering (IEEE Cat. No.99CB37002) . 597–607. DOI: http://dx.doi.org/10.1145/302405.302710

    work page doi:10.1145/302405.302710 1999

  19. [19]

    Keiren, Vincent J.J

    Yi Ling Hwong, Jeroen J.A. Keiren, Vincent J.J. Kusters , Sander Leemans, and Tim A.C. Willemse. 2013. Formalising and analysing the c ontrol soft- ware of the Compact Muon Solenoid Experiment at the Large Had ron Col- lider. Science of Computer Programming 78, 12 (2013), 2435 – 2452. DOI: http://dx.doi.org/https://doi.org/10.1016/j.scico.2012.11.009 Spec...

    work page doi:10.1016/j.scico.2012.11.009 2013

  20. [20]

    Ranjit Jhala and Rupak Majumdar. 2009. Software Model C heck- ing. ACM Comput. Surv. 41, 4, Article 21 (Oct 2009), 54 pages. DOI: http://dx.doi.org/10.1145/1592434.1592438

    work page doi:10.1145/1592434.1592438 2009

  21. [21]

    Leslie Lamport. 1979. How to Make a Multiprocessor Comp uter That Correctly Executes Multiprocess Programs. IEEE Trans. Comput. C-28, 9 (Sep. 1979), 690–

    work page 1979

  22. [22]

    DOI:http://dx.doi.org/10.1109/TC.1979.1675439

    work page doi:10.1109/tc.1979.1675439 1979

  23. [23]

    Leslie Lamport. 2002. Specifying systems: the TLA+ language and tools for hard- ware and software engineers . Addison-Wesley

    work page 2002

  24. [24]

    Lång and others

    J.L. Lång and others. 2018. ADAPOS: An Architecture for Publishing AL- ICE DCS Conditions Data. In Proc. of International Conference on Accelera- tor and Large Experimental Physics Control Systems (ICALEPC S’17), Barcelona, Spain, 8-13 October 2017 (International Conference on Acce lerator and Large Experimental Control Systems) . JACoW, Geneva, Switzerla...

    work page doi:10.18429/jacow-icalepcs2017-tupha042 2018

  25. [25]

    Amir Pnueli. 1977. The temporal logic of programs. (Oct 1977). DOI: http://dx.doi.org/10.1109/SFCS.1977.32

    work page doi:10.1109/sfcs.1977.32 1977

  26. [26]

    Petr Rockai, Ivana Cerná, and Jiri Barnat. 2017. DiVM: M odel Checking with LLVM and Graph Memory. CoRR abs/1703.05341 (2017). arXiv: 1703.05341 http://arxiv.org/abs/1703.05341

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  27. [27]

    Kristin Y. Rozier. 2011. Linear Temporal Logic Symboli c Model Checking. Computer Science Review 5, 2 (2011), 163 – 203. DOI: http://dx.doi.org/https://doi.org/10.1016/j.cosrev.2010.06.002

    work page doi:10.1016/j.cosrev.2010.06.002 2011

  28. [28]

    Wing and Mandana Vaziri-Farahani

    Jeannette M. Wing and Mandana Vaziri-Farahani. 1997. A case study in model checking software systems. Science of Computer Programming 28, 2 (1997), 273 –

    work page 1997

  29. [29]

    DOI:http://dx.doi.org/https://doi.org/10.1016/S0167-6423(96)00020-2 For- mal Specifications: Foundations, Methods, Tools and Applic ations

    work page doi:10.1016/s0167-6423(96)00020-2