ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 14:30 - 15:00 at JUPITER - Software Verification II Chair(s): Heike Wehrheim

Variability models allow effective building of many custom model variants for various configurations. Lifted model checking for a variability model is capable of verifying all its variants simultaneously in a single run by exploiting the similarities between the variants. The computational cost of lifted model checking still greatly depends on the number of variants (the size of configuration space), which is often huge. 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.

Wed 10 Apr

fase-2019-papers
14:00 - 16:00: FASE 2019 - Software Verification II at JUPITER
Chair(s): Heike WehrheimPaderborn University
fase-2019-papers14:00 - 14:30
Talk
Link to publication
fase-2019-papers14:30 - 15:00
Talk
Aleksandar S. DimovskiMother Teresa University, Skopje, Axel LegayINRIA Rennes, Andrzej WąsowskiIT University of Copenhagen, Denmark
Link to publication
fase-2019-papers15:00 - 15:30
Talk
Huang Li, Eun-Young KangUniversity of Southern Denmark
Link to publication
fase-2019-papers15:30 - 16:00
Talk
Himanshu Arora, Raghavan KomondoorIndian Institute of Science, Bangalore, G. RamalingamMicrosoft Research
Link to publication