Coherent branching feature bisimulation
This work addresses the challenge of efficiently analyzing behavioral properties in software product lines, though it is incremental as it builds on existing bisimulation theory for labeled transition systems.
The paper tackles the problem of behavioral analysis for software product lines by proposing a new behavioral equivalence called branching feature bisimulation for feature transition systems, which generalizes branching bisimulation for labeled transition systems. The result includes a minimization algorithm for a restricted notion, and its application in a small case study shows a significant speed-up in model checking of behavioral properties.
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.