HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Using an SMT Solver for Checking the Completeness of FSM-Based Tests

Abstract : Deriving tests with guaranteed fault coverage by FSM-based test methods is rather complex for systems with a large number of states. At the same time, formal verification methods allow to effectively process large transition systems; in particular, SMT solvers are widely used to solve analysis problems for finite transition systems. In this paper, we describe the known necessary and sufficient conditions of completeness of test suites derived by FSM-based test methods via the first-order logic formulas and use an SMT solver in order to check them. In addition, we suggest a new sufficient condition for test suite completeness and check the corresponding first-order logic formula via the SMT solver. The results of computer experiments with randomly generated finite state machines confirm the correctness and efficiency of a proposed approach.
Complete list of metadata

Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, May 27, 2021 - 4:42:16 PM
Last modification on : Thursday, May 27, 2021 - 4:58:44 PM
Long-term archiving on: : Saturday, August 28, 2021 - 7:58:11 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Evgenii Vinarskii, Andrey Laputenko, Nina Yevtushenko. Using an SMT Solver for Checking the Completeness of FSM-Based Tests. 32th IFIP International Conference on Testing Software and Systems (ICTSS), Dec 2020, Naples, Italy. pp.289-295, ⟨10.1007/978-3-030-64881-7_18⟩. ⟨hal-03239812⟩



Record views