$$\hbox {CTL}^{\star }$$ family-based model checking using variability abstractions and modal transition systems
Autor: | Aleksandar S. Dimovski |
---|---|
Rok vydání: | 2019 |
Předmět: |
Model checking
Theoretical computer science Computer science 020207 software engineering 02 engineering and technology Star (graph theory) DUAL (cognitive architecture) Variable (computer science) Modal Development (topology) Theory of computation 0202 electrical engineering electronic engineering information engineering Configuration space Software Information Systems |
Zdroj: | International Journal on Software Tools for Technology Transfer. 22:35-55 |
ISSN: | 1433-2787 1433-2779 |
Popis: | Variational systems can produce a (potentially huge) number of related systems, known as products or variants, by using features (configuration options) to mark the variable functionality. In many of the application domains, their rigorous verification and analysis are very important, yet the appropriate tools rarely are able to analyse variational systems. Recently, this problem was addressed by designing specialized so-called family-based model checking algorithms, which allow simultaneous verification of all variants in a single run by exploiting the commonalities between the variants. Yet, their computational cost still greatly depends on the number of variants (the size of configuration space), which is often huge. Moreover, their implementation and maintenance represent a costly research and development task. One of the most promising approaches to fighting the configuration space explosion problem is variability abstractions, which simplify variability away from variational systems. In this work, we show how to achieve efficient family-based model checking of $$\hbox {CTL}^{\star }$$ temporal properties using variability abstractions and off-the-shelf (single-system) tools. We use variability abstractions for deriving abstract family-based model checking, where the variability model of a variational system is replaced with an abstract (smaller) version of it, called modal transition system, which preserves the satisfaction of both universal and existential temporal properties, as expressible in $$\hbox {CTL}^{\star }$$. Modal transition systems contain two kinds of transitions, termed may- and must-transitions, which are defined by the conservative (over-approximating) abstractions and their dual (under-approximating) abstractions, respectively. The variability abstractions can be combined with different partitionings of the configuration space to infer suitable divide-and-conquer verification plans for the given variational system. We illustrate the practicality of this approach for several variational systems using the standard version of (single-system) NuSMV model checker. |
Databáze: | OpenAIRE |
Externí odkaz: |