Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 285)
Detail práce
   Přihlásit přes CAS
Řešení problému exploze stavového prostoru při generování testů s použitím model checkeru
Název práce v češtině: Řešení problému exploze stavového prostoru při generování testů s použitím model checkeru
Název v anglickém jazyce: Řešení problému exploze stavového prostoru při generování testů s použitím model checkeru
Klíčová slova anglicky: test case generation, model-based testing, state explosion problem, abstraction
Akademický rok vypsání: 2018/2019
Typ práce: diplomová práce
Jazyk práce: angličtina
Ústav: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
Vedoucí / školitel: Paolo Arcaini, Ph.D.
Řešitel:
Zásady pro vypracování
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.
Seznam odborné literatury
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.
 
Univerzita Karlova | Informační systém UK