Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL
(2019)
Files
No attached file found for this publication.
Details
- Authors
Dimovski, Aleksandar S. 
Wasowski, Andrzej
- Abstract
- One of the most promising approaches to fighting the configuration space explosion problem in lifted model checking are variability abstractions. In this work, we define a novel game-based approach for variability-specific abstraction and refinement for lifted model checking of the full CTL, interpreted over 3-valued semantics. We propose a direct algorithm for solving a 3-valued (abstract) lifted model checking game. In case the result of model checking an abstract variability model is indefinite, we suggest a new notion of refinement, which eliminates indefinite results. This provides an iterative incremental variability-specific abstraction and refinement framework, where refinement is applied only where indefinite results exist and definite results from previous iterations are reused. The practicality of this approach is demonstrated on several variability models.
- Affiliations
Citations
Dimovski, A. S., Legay, A., & Wasowski, A. (2019). Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL. FASE 2019. Published. https://doi.org/10.1007/978-3-030-16722-6_11 (Original work published 2019)