Coherent branching feature bisimulation

TL;DR

This paper introduces a new behavioral equivalence for feature transition systems that generalizes branching bisimulation, along with a minimization algorithm that improves model checking efficiency despite intractability.

Contribution

It proposes a generalized branching bisimulation for feature transition systems and presents a minimization algorithm with proven correctness for coherent cases.

Findings

Branching feature bisimulation coincides with individual product bisimulation.

A correct minimization algorithm is developed for coherent branching feature bisimulation.

Application of the algorithm speeds up model checking in a case study.

Abstract

Progress in the behavioral analysis of software product lines at the family level benefits from further development of the underlying semantical theory. Here, we propose a behavioral equivalence for feature transition systems (FTS) generalizing branching bisimulation for labeled transition systems (LTS). We prove that branching feature bisimulation for an FTS of a family of products coincides with branching bisimulation for the LTS projection of each the individual products. For a restricted notion of coherent branching feature bisimulation we furthermore present a minimization algorithm and show its correctness. Although the minimization problem for coherent branching feature bisimulation is shown to be intractable, application of the algorithm in the setting of a small case study results in a significant speed-up of model checking of behavioral properties.