×

zbMATH — the first resource for mathematics

Abstract family-based model checking using modal featured transition systems: preservation of \(\mathrm{CTL}^{\star}\). (English) Zbl 1423.68277
Russo, Alessandra (ed.) et al., Fundamental approaches to software engineering. 21st international conference, FASE 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10802, 301-318 (2018).
Summary: Variational systems allow effective building of many custom variants by using features (configuration options) to mark the variable functionality. In many of the applications, their quality assurance and formal verification are of paramount importance. Family-based model checking allows simultaneous verification of all variants of a variational system in a single run by exploiting the commonalities between the variants. Yet, its computational cost still greatly depends on the number of variants (often huge).
In this work, we show how to achieve efficient family-based model checking of \(\mathrm{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 featured transition system, which preserves the satisfaction of both universal and existential temporal properties, as expressible in \(\mathrm{CTL}^{\star}\). Modal featured 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 set of variants to infer suitable divide-and-conquer verification plans for the variational system. We illustrate the practicality of this approach for several variational systems.
For the entire collection see [Zbl 1408.68023].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI