Thesis (Selection of subject)Thesis (Selection of subject)(version: 285)
Assignment details
   Login via CAS
Řešení problému exploze stavového prostoru při generování testů s použitím model checkeru
Thesis title in Czech: Řešení problému exploze stavového prostoru při generování testů s použitím model checkeru
Thesis title in English: Řešení problému exploze stavového prostoru při generování testů s použitím model checkeru
English key words: test case generation, model-based testing, state explosion problem, abstraction
Academic year of topic announcement: 2018/2019
Type of assignment: diploma thesis
Thesis language: angličtina
Department: Department of Distributed and Dependable Systems (32-KDSS)
Supervisor: Paolo Arcaini, Ph.D.
Author:
Guidelines
One of the well-known techniques for model-based test generation exploits the capability of model checkers to return counterexamples upon property violations. However, this approach is not always optimal in practice due to the required time and memory, or even not feasible due to the state explosion problem of model checking. A way to mitigate these limitations consists in decomposing (exploiting variables dependency) a system model into suitable subsystem models. Tests are built for the single subsystems and combined in order to obtain a test for the whole system.

The aim of the thesis is to automatize the approach for specifications of the NuSMV model checker.
Starting from a test goal, the variables involved in the test goal must be identified. Then, dependencies among variables and strongly connected components of variables must be found. Given the partition of the variables in strongly connected components, different (smaller) NuSMV models must be obtained. Finally, sequences must be derived from the models and combined to obtain a test for the whole system.
References
A. Gargantini and C. Heitmeyer. Using model checking to generate tests from requirements specifications. In Proceedings of ESEC/FSE'99, volume 1687 of Lecture Notes in Computer Science, pages 146–162, London, UK, 1999. Springer Berlin Heidelberg.

P. Arcaini, A. Gargantini, and E. Riccobene. An abstraction technique for testing decomposable systems by model checking. In M. Seidl and N. Tillmann, editors, Tests and Proofs, volume 8570 of Lecture Notes in Computer Science, pages 36–52. Springer International Publishing, 2014.

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html