pith. sign in

arxiv: 1907.11895 · v1 · pith:IFCL3ZUQnew · submitted 2019-07-27 · 💻 cs.SE · cs.FL

Combining closed-loop test generation and execution by means of model checking

Igor Buzhinsky , Valeriy Vyatkin This is my paper

Pith reviewed 2026-05-24 14:56 UTC · model grok-4.3

classification 💻 cs.SE cs.FL
keywords model checkingtest generationclosed-loopindustrial automationhybrid verificationsystem coveragerequirement verification
0
0 comments X

The pith

A framework verifies automation systems by model checking requirements only on coverage-achieving test behaviors in closed-loop models.

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

The paper establishes a hybrid framework that uses model checking on selected behaviors from a test suite rather than the full state space to verify industrial automation systems. This approach supports closed-loop models including both controller and plant. It seeks to balance the high reliability of model checking with the lower computational cost of testing. The method generates test suites that cover both the system and its requirements, then checks those behaviors formally. This matters for complex systems where exhaustive verification is impossible but reliability is required.

Core claim

Instead of full model checking, system requirements are checked only on particular system behaviors which represent a test suite achieving coverage for both the system and the requirements, in the context of closed-loop models where the plant is also modeled.

What carries the argument

The hybrid verification framework combining test generation, execution, and model checking on coverage test suites for closed-loop automation systems.

If this is right

  • Verification of complex systems becomes computationally feasible while retaining formal guarantees on covered behaviors.
  • Both system behaviors and requirement satisfaction are addressed through the same coverage-achieving test suite.
  • Closed-loop modeling allows the verification to account for interactions between controller and plant.
  • Test generation and model checking are integrated into one framework rather than used separately.

Where Pith is reading between the lines

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

  • This method might be applicable to other safety-critical systems beyond industrial automation.
  • Optimizing the coverage criteria could further improve the reliability-complexity trade-off.
  • Integration with existing test tools could make the framework more practical for engineers.

Load-bearing premise

That checking the requirements on the behaviors in the coverage test suite is sufficient to ensure the overall reliability of the system.

What would settle it

An example of a closed-loop automation system where a requirement is violated on a behavior not in the test suite, but would be detected by exhaustive model checking.

read the original abstract

Model checking is an established technique to formally verify automation systems which are required to be trusted. However, for sufficiently complex systems model checking becomes computationally infeasible. On the other hand, testing, which offers less reliability, often does not present a serious computational challenge. Searching for synergies between these two approaches, this paper proposes a framework to ensure reliability of industrial automation systems by means of hybrid use of model checking and testing. This framework represents a way to achieve a trade-off between verification reliability and computational complexity which has not yet been explored in other approaches. Instead of undergoing usual model checking, system requirements are checked only on particular system behaviors which represent a test suite achieving coverage for both the system and the requirements. Then, all stages of the framework support the case of a closed-loop model, where not only the controller, but also the plant is modeled.

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 proposes a framework for hybrid use of model checking and testing to verify industrial automation systems. It aims to achieve a trade-off between verification reliability and computational complexity by checking system requirements only on particular system behaviors from a test suite that achieves coverage for both the system and the requirements, supporting closed-loop models where both controller and plant are modeled.

Significance. If the coverage definition can be shown to guarantee that all requirement-violating traces appear in the test suite, the framework could provide a useful practical compromise for systems too complex for exhaustive model checking. The explicit support for closed-loop models aligns with industrial needs.

major comments (2)
  1. [Abstract] Abstract, paragraph 3: the claim that model checking restricted to behaviors in a coverage-achieving test suite suffices for overall reliability lacks any argument or construction showing that the chosen coverage criteria (for system and requirements) must include every counterexample trace to an LTL/CTL property; standard coverage metrics do not guarantee this.
  2. [Abstract] Abstract: the central trade-off claim rests on the unproven premise that the finite test suite captures all requirement violations, yet no definition of the coverage relation or proof of completeness is supplied to close the gap between coverage and exhaustive verification.
minor comments (1)
  1. The manuscript description remains at a high level with no concrete algorithm, pseudocode, or evaluation data, making assessment of the framework's practicality difficult.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the careful reading and the identification of important points regarding the claims made in the abstract. We address each major comment below and agree that revisions are required to better scope the contribution.

read point-by-point responses

  1. Referee: [Abstract] Abstract, paragraph 3: the claim that model checking restricted to behaviors in a coverage-achieving test suite suffices for overall reliability lacks any argument or construction showing that the chosen coverage criteria (for system and requirements) must include every counterexample trace to an LTL/CTL property; standard coverage metrics do not guarantee this.

    Authors: We agree that the current manuscript provides no formal argument or construction establishing that the coverage criteria necessarily capture every counterexample trace. The framework is presented as a practical hybrid method that performs model checking only on the behaviors present in a coverage-achieving test suite, thereby obtaining a trade-off rather than exhaustive verification. We will revise the abstract (and relevant sections) to remove any implication of overall reliability and to explicitly state that verification is limited to the covered behaviors. revision: yes

  2. Referee: [Abstract] Abstract: the central trade-off claim rests on the unproven premise that the finite test suite captures all requirement violations, yet no definition of the coverage relation or proof of completeness is supplied to close the gap between coverage and exhaustive verification.

    Authors: The referee is correct that the manuscript supplies neither an explicit definition of the coverage relation used nor a completeness proof relating coverage to the set of all violating traces. The paper describes the overall framework, its support for closed-loop models, and the use of coverage-achieving suites, but does not close this theoretical gap. We will revise the abstract and add a short discussion of the scope and limitations of the approach to avoid overstating the guarantees. revision: yes

standing simulated objections not resolved
  • Providing a proof or construction that standard coverage criteria for system and requirements must include every counterexample trace to arbitrary LTL/CTL properties (this would require new theoretical results beyond the framework description in the current manuscript).

Circularity Check

0 steps flagged

No circularity in framework proposal

full rationale

The paper presents a methodological framework for hybrid model checking and testing on closed-loop models, checking requirements only on coverage-achieving test suites. No equations, fitted parameters, predictions, or derivations appear in the provided text or abstract. The central claim is an explicit trade-off proposal with a stated assumption about coverage sufficiency; it does not reduce any result to its inputs by construction, self-definition, or self-citation chain. The skeptic concern addresses a potential gap in the coverage argument (correctness risk) rather than circularity. This is a self-contained framework description with no load-bearing self-referential steps.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Review performed on abstract only; no free parameters, axioms, or invented entities are described in the provided text.

pith-pipeline@v0.9.0 · 5670 in / 1062 out tokens · 20727 ms · 2026-05-24T14:56:51.299586+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

36 extracted references · 36 canonical work pages

  1. [1]

    Journal of Automated Reasoning 45(4), 397–414 (2010)

    Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. Journal of Automated Reasoning 45(4), 397–414 (2010)

    work page 2010

  2. [2]

    IEEE Transactions on Software Engineering 41(5), 507– 525 (2015)

    Barr, E.T., Harman, M., McMinn, P., Shahbaz, M., Yoo, S.: The oracle problem in software testing: A survey. IEEE Transactions on Software Engineering 41(5), 507– 525 (2015)

    work page 2015

  3. [3]

    Formal Methods in System Design 40(1), 20–40 (2012)

    Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. Formal Methods in System Design 40(1), 20–40 (2012)

    work page 2012

  4. [4]

    Advances in Computers, Elsevier 58, 117–148 (2003)

    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers, Elsevier 58, 117–148 (2003)

    work page 2003

  5. [5]

    (eds.): Model-based testing of reactive sys- tems: advanced lectures

    Broy, M., Jonsson, B., Katoen, J.P., Leucker, M., Pretschner, A. (eds.): Model-based testing of reactive sys- tems: advanced lectures. Lecture Notes in Computer Sci- ence, vol. 3472. Springer (2005)

    work page 2005

  6. [6]

    Information and Computation 98(2), 142–170 (1992)

    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10 20 states and beyond. Information and Computation 98(2), 142–170 (1992)

    work page 1992

  7. [7]

    In: 2015 IEEE Trustcom/BigDataSE/ISPA, vol

    Buzhinsky, I., Pang, C., Vyatkin, V.: Formal modeling of testing software for cyber-physical automation systems. In: 2015 IEEE Trustcom/BigDataSE/ISPA, vol. 3, pp. 301–306. IEEE (2015)

    work page 2015

  8. [8]

    IEEE Transactions on Industrial Informatics 13(4), 1521–1530 (2017)

    Buzhinsky, I., Vyatkin, V.: Automatic inference of finite- state plant models from traces and temporal proper- ties. IEEE Transactions on Industrial Informatics 13(4), 1521–1530 (2017)

    work page 2017

  9. [9]

    In: 22th IEEE Confer- ence on Emerging Technologies and Factory Automation (ETFA)

    Buzhinsky, I., Vyatkin, V.: Testing automation systems by means of model checking. In: 22th IEEE Confer- ence on Emerging Technologies and Factory Automation (ETFA). IEEE (2017)

    work page 2017

  10. [10]

    International Journal on Software Tools for Technology Transfer 2(4), 410–425 (2000)

    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer 2(4), 410–425 (2000)

    work page 2000

  11. [11]

    MIT press (1999)

    Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT press (1999)

    work page 1999

  12. [12]

    Periodica Polytech- nica

    Darvas, D., Majzik, I., Vi˜ nuela, E.B.: PLC program translation for verification purposes. Periodica Polytech- nica. Electrical Engineering and Computer Science61(2), 151–165 (2017)

    work page 2017

  13. [13]

    In: Service Orientation in Holonic and Multi-Agent Man- ufacturing, pp

    Drozdov, D., Patil, S., Vyatkin, V.: Formal modelling of distributed automation CPS with CP-agnostic software. In: Service Orientation in Holonic and Multi-Agent Man- ufacturing, pp. 35–46. Springer (2017)

    work page 2017

  14. [14]

    In: 14th Brazilian Sympo- sium on Formal Methods: Short Papers, pp

    Duarte, L.: Integrating software testing and model check- ing through model extraction. In: 14th Brazilian Sympo- sium on Formal Methods: Short Papers, pp. 73–78 (2011)

    work page 2011

  15. [15]

    Journal of Sys- tems and Software 82(9), 1403–1418 (2009)

    Fraser, G., Wotawa, F., Ammann, P.: Issues in using model checkers for test case generation. Journal of Sys- tems and Software 82(9), 1403–1418 (2009)

    work page 2009

  16. [16]

    Software Testing, Verification and Reliability 19(3), 215–261 (2009)

    Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Software Testing, Verification and Reliability 19(3), 215–261 (2009)

    work page 2009

  17. [17]

    In: IEEE International Conference on Systems, Man, and Cybernetics (SMC), vol

    Frey, G., Litz, L.: Formal methods in PLC programming. In: IEEE International Conference on Systems, Man, and Cybernetics (SMC), vol. 4, pp. 2431–2436. IEEE (2000)

    work page 2000

  18. [18]

    In: 8th International Workshop on Discrete Event Systems (WODES), pp

    Gourcuff, V., De Smet, O., Faure, J.M.: Efficient repre- sentation for formal verification of PLC programs. In: 8th International Workshop on Discrete Event Systems (WODES), pp. 182–187. IEEE (2006)

    work page 2006

  19. [19]

    IFAC Proceedings Volumes 41(2), 5101–5106 (2008)

    Gourcuff, V., De Smet, O., Faure, J.M.: Improving large- sized PLC programs verification using abstractions. IFAC Proceedings Volumes 41(2), 5101–5106 (2008)

    work page 2008

  20. [20]

    In: International Workshop on Formal Approaches to Software Testing, pp

    Heimdahl, M.P., Rayadurgam, S., Visser, W., Devaraj, G., Gao, J.: Auto-generating test sequences using model checkers: A case study. In: International Workshop on Formal Approaches to Software Testing, pp. 42–59. Springer (2003)

    work page 2003

  21. [21]

    IEEE Trans- actions on Software Engineering 23(5), 279–295 (1997)

    Holzmann, G.J.: The model checker SPIN. IEEE Trans- actions on Software Engineering 23(5), 279–295 (1997)

    work page 1997

  22. [22]

    In: International Confer- ence on Tools and Algorithms for the Construction and Analysis of Systems, pp

    Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language- independent model checking. In: International Confer- ence on Tools and Algorithms for the Construction and Analysis of Systems, pp. 692–707. Springer (2015)

    work page 2015

  23. [23]

    Interna- tional Journal on Software Tools for Technology Transfer 2(4), 328–342 (2000)

    Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Interna- tional Journal on Software Tools for Technology Transfer 2(4), 328–342 (2000)

    work page 2000

  24. [24]

    The Journal of Logic and Algebraic Pro- gramming 78(5), 293–303 (2009)

    Leucker, M., Schallhart, C.: A brief account of runtime verification. The Journal of Logic and Algebraic Pro- gramming 78(5), 293–303 (2009)

    work page 2009

  25. [25]

    In: 8th International Conference on Informatics in Control, Automation and Robotics (ICINCO), pp

    Maier, A., Vodencarevic, A., Niggemann, O., Just, R., Jaeger, M.: Anomaly detection in production plants us- ing timed automata. In: 8th International Conference on Informatics in Control, Automation and Robotics (ICINCO), pp. 363–369 (2011)

    work page 2011

  26. [26]

    Software & Systems Modeling 15(4), 937– 960 (2016)

    Ovatman, T., Aral, A., Polat, D., ¨Unver, A.O.: An overview of model checking practices on verification of PLC software. Software & Systems Modeling 15(4), 937– 960 (2016)

    work page 2016

  27. [27]

    In: 10th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC & HMIT 2017), pp

    Pakonen, A., Tahvonen, T., Hartikainen, M., Pihlanko, M.: Practical applications of model checking in the Finnish nuclear industry. In: 10th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC & HMIT 2017), pp. 1342–1352. American Nuclear Society (2017)

    work page 2017

  28. [28]

    In: 13th IEEE International Confer- ence on Industrial Informatics (INDIN), pp

    Patil, S., Vyatkin, V., Pang, C.: Counterexample-guided simulation framework for formal verification of flexible automation systems. In: 13th IEEE International Confer- ence on Industrial Informatics (INDIN), pp. 1192–1197. IEEE (2015) Combining closed-loop test generation and execution by means of model checking 15

    work page 2015

  29. [29]

    Preuße, S.: Technologies for Engineering Manufacturing Systems Control in Closed Loop, vol. 10. Logos Verlag Berlin GmbH (2013)

    work page 2013

  30. [30]

    In: 17th IEEE Conference on Emerging Technologies and Factory Au- tomation (ETFA), pp

    Preuße, S., Lapp, H., Hanisch, H.: Closed-loop system modeling, validation, and verification. In: 17th IEEE Conference on Emerging Technologies and Factory Au- tomation (ETFA), pp. 1–8. IEEE (2012)

    work page 2012

  31. [31]

    Journal of Software Engineering and Ap- plications 8(9), 499–519 (2015)

    R¨ osch, S., Ulewicz, S., Provost, J., Vogel-Heuser, B.: Re- view of model-based testing approaches in production au- tomation and adjacent domains—current challenges and research gaps. Journal of Software Engineering and Ap- plications 8(9), 499–519 (2015)

    work page 2015

  32. [32]

    In: 37th International Conference on Software Engineering – Volume 1, pp

    Su, T., Fu, Z., Pu, G., He, J., Su, Z.: Combining symbolic execution and model checking for data flow testing. In: 37th International Conference on Software Engineering – Volume 1, pp. 654–665. IEEE (2015)

    work page 2015

  33. [33]

    In: 2004 IEEE International Conference on Information Reuse and Integration (IRI), pp

    Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: 2004 IEEE International Conference on Information Reuse and Integration (IRI), pp. 483–498. IEEE (2004)

    work page 2004

  34. [34]

    Proceedings of the IEEE 104(5), 960–972 (2016)

    Tripakis, S.: Compositionality in the science of system design. Proceedings of the IEEE 104(5), 960–972 (2016)

    work page 2016

  35. [35]

    In: 8th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), vol

    Vyatkin, V., Hanisch, H.M.: Formal modeling and ver- ification in the software engineering framework of IEC 61499: a way to self-verifying systems. In: 8th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), vol. 2, pp. 113–118. IEEE (2001)

    work page 2001

  36. [36]

    In: 13th IEEE International Conference on Information Reuse and Integration (IRI), pp

    Zeng, B., Tan, L.: Test criteria for model-checking- assisted test case generation: a computational study. In: 13th IEEE International Conference on Information Reuse and Integration (IRI), pp. 600–607. IEEE (2012)

    work page 2012