Towards a Feature mu-Calculus Targeting SPL Verification

TL;DR

This paper introduces two new variants of the mu-calculus tailored for feature transition systems, enabling product-specific and family-based verification of software product lines.

Contribution

The paper proposes mu-Lf and mu-Lf' logics that incorporate feature expressions, extending the mu-calculus for SPL verification and relating them to existing mu-calculus.

Findings

Formal semantics for mu-Lf and mu-Lf' are provided.

Application demonstrated through a toy example of property model checking.

Embedding of mu-Lf' into mu-calculus with data shown.

Abstract

The modal mu-calculus mu-L is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the mu-calculus, mu-Lf and mu-Lf', for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific products and subfamilies. We provide semantics for mu-Lf and mu-Lf' and relate the two new mu-calculi and mu-L to each other. Next, we focus on the analysis of SPL behavior and show how our formalism can be applied for product-based verification with mu-Lf as well as family-based verification with mu-Lf'. We illustrate by means of a toy example how properties can be model checked, exploiting an embedding of mu-Lf' into the mu-calculus with data.