Back to Search
Start Over
Using an SMT Solver for Checking the Completeness of FSM-Based Tests
- Source :
- Lecture Notes in Computer Science, 32th IFIP International Conference on Testing Software and Systems (ICTSS), 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⟩, Testing Software and Systems ISBN: 9783030648800, ICTSS
- Publication Year :
- 2020
- Publisher :
- HAL CCSD, 2020.
-
Abstract
- Part 5: Short Contributions; International audience; 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.
- Subjects :
- 021103 operations research
Correctness
Finite-state machine
Computer science
0211 other engineering and technologies
020207 software engineering
02 engineering and technology
Computer experiment
FSM based testing
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI]
Satisfiability modulo theories
SMT solver
Fault coverage
0202 electrical engineering, electronic engineering, information engineering
Test suite
[INFO]Computer Science [cs]
Fist order logic formulas
Completeness (statistics)
Algorithm
Formal verification
Subjects
Details
- Language :
- English
- ISBN :
- 978-3-030-64880-0
- ISBNs :
- 9783030648800
- Database :
- OpenAIRE
- Journal :
- Lecture Notes in Computer Science, 32th IFIP International Conference on Testing Software and Systems (ICTSS), 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⟩, Testing Software and Systems ISBN: 9783030648800, ICTSS
- Accession number :
- edsair.doi.dedup.....40249ed3ff5fe21c966d4059d0eb61b6