Tessa Belder (TU/e, Eindhoven, The Netherlands) |
Maurice H. ter Beek (ISTI-CNR, Pisa, Italy) |
Erik P. de Vink (TU/e, Eindhoven and CWI, Amsterdam, The Netherlands) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.182.2 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |