Using an SMT Solver for Checking the Completeness of FSM-Based Tests - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

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

Résumé

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.
Fichier principal
Vignette du fichier
497758_1_En_18_Chapter.pdf (132.85 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03239812 , version 1 (27-05-2021)

Licence

Paternité

Identifiants

Citer

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⟩
40 Consultations
55 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More