%0 Conference Proceedings
%T Using an SMT Solver for Checking the Completeness of FSM-Based Tests
%+ Lomonosov Moscow State University (MSU)
%+ Tomsk State University [Tomsk]
%+ Institute for System Programming of the Russian Academy of Sciences [Moscow] (ISPRAS)
%A Vinarskii, Evgenii
%A Laputenko, Andrey
%A Yevtushenko, Nina
%Z Part 5: Short Contributions
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 32th IFIP International Conference on Testing Software and Systems (ICTSS)
%C Naples, Italy
%Y Valentina Casola
%Y Alessandra De Benedictis
%Y Massimiliano Rak
%I Springer International Publishing
%3 Testing Software and Systems
%V LNCS-12543
%P 289-295
%8 2020-12-09
%D 2020
%R 10.1007/978-3-030-64881-7_18
%K FSM based testing
%K SMT solver
%K Fist order logic formulas
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03239812/document
%2 https://inria.hal.science/hal-03239812/file/497758_1_En_18_Chapter.pdf
%L hal-03239812
%U https://inria.hal.science/hal-03239812
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-ICTSS
%~ IFIP-LNCS-12543