Specification-based Test Generation and Optimization Using Model Checking

2007 ◽  
Author(s):  
Hongwei Zeng ◽  
Huaikou Miao ◽  
Jing Liu
Keyword(s):  
Model Checking ◽  
Test Generation

scholarly journals Test generation from P systems using model checking

2010 ◽  
Vol 79 (6) ◽  
pp. 350-362 ◽  
Author(s):  
Florentin Ipate ◽  
Marian Gheorghe ◽  
Raluca Lefticaru
Keyword(s):  
Model Checking ◽  
Test Generation ◽  
P Systems

scholarly journals Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking

2010 ◽  
Vol 36 (4) ◽  
pp. 474-494 ◽  
Author(s):  
S Artzi ◽  
A Kiezun ◽  
J Dolby ◽  
F Tip ◽  
D Dig ◽  
...  
Keyword(s):  
Model Checking ◽  
Test Generation ◽  
Web Applications ◽  
Dynamic Test ◽  
State Model

scholarly journals Mutation-Based Test Generation for PLC Embedded Software Using Model Checking

2016 ◽  
pp. 155-171 ◽  
Author(s):  
Eduard P. Enoiu ◽  
Daniel Sundmark ◽  
Adnan Čaušević ◽  
Robert Feldt ◽  
Paul Pettersson
Keyword(s):  
Model Checking ◽  
Test Generation ◽  
Embedded Software

scholarly journals Cooperative verifier-based testing with CoVeriTest

2021 ◽  
Author(s):  
Dirk Beyer ◽  
Marie-Christine Jakobs
Keyword(s):  
Model Checking ◽  
Test Generation ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Test Suite ◽  
Hybrid Technique ◽  
Conditional Model ◽  
Level Information ◽  
High Level ◽  
Test Suite Generation

AbstractTesting is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15%).

Sign in / Sign up

Export Citation Format

Share Document