TY - JOUR

T1 - Generalized abstraction-refinement for game-based CTL lifted model checking

AU - Dimovski, Aleksandar

AU - Wasowski, Andrzej

AU - Legay, Axel

PY - 2020

Y1 - 2020

N2 - System families (Software Product Lines) are becoming omnipresent in application areas ranging from embedded system domains to system-level software and communication protocols. Software Product Line methods and architectures allow effective building many custom variants of a software system in these domains. In many of the applications, their rigorous verification and quality assurance are of paramount importance. Lifted model checking for system families is capable of verifying all their 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. Variability abstractions have successfully addressed this configuration space explosion problem, giving rise to smaller abstract variability models with fewer abstract configurations. Abstract variability models are given as modal transition systems, which contain may (over-approximating) and must (under-approximating) transitions. Thus, they preserve both universal and existential CTL properties.In this work, we bring two main contributions. First, 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. Second, we propose a new generalized definition of abstract variability models, given as so-called generalized modal transition systems, by introducing the notion of (must) hyper-transitions. This results in more precise abstract models in which more CTL formulae can be proved or disproved. We integrate the newly defined generalized abstract variability models in the existing abstraction-refinement framework for game-based lifted model checking of CTL. Finally, we evaluate the practicality of this approach on several system families.

AB - System families (Software Product Lines) are becoming omnipresent in application areas ranging from embedded system domains to system-level software and communication protocols. Software Product Line methods and architectures allow effective building many custom variants of a software system in these domains. In many of the applications, their rigorous verification and quality assurance are of paramount importance. Lifted model checking for system families is capable of verifying all their 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. Variability abstractions have successfully addressed this configuration space explosion problem, giving rise to smaller abstract variability models with fewer abstract configurations. Abstract variability models are given as modal transition systems, which contain may (over-approximating) and must (under-approximating) transitions. Thus, they preserve both universal and existential CTL properties.In this work, we bring two main contributions. First, 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. Second, we propose a new generalized definition of abstract variability models, given as so-called generalized modal transition systems, by introducing the notion of (must) hyper-transitions. This results in more precise abstract models in which more CTL formulae can be proved or disproved. We integrate the newly defined generalized abstract variability models in the existing abstraction-refinement framework for game-based lifted model checking of CTL. Finally, we evaluate the practicality of this approach on several system families.

U2 - 10.1016/j.tcs.2020.06.011

DO - 10.1016/j.tcs.2020.06.011

M3 - Journal article

VL - 837

SP - 181

EP - 206

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -