Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL* (Extended Version)

TL;DR

This paper introduces a novel family-based model checking approach for CTL* properties using variability abstractions and modal featured transition systems, enabling more efficient verification of large variational systems.

Contribution

It presents a new abstraction technique with modal featured transition systems that preserves CTL* properties, improving the efficiency of family-based model checking.

Findings

Effective abstraction preserves CTL* satisfaction

Combining abstractions with variant partitioning improves scalability

Practical verification demonstrated on several variational systems

Abstract

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 CTL* 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 CTL*. 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.