Coherent branching feature bisimulation

T. Belder, M.H. Beek, ter, E.P. Vink, de

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)
76 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings 6th Workshop on Formal Methods and Analysis in SPL Engineering (FMSPLE 2015, London, UK, April 11, 2015)
EditorsJ.M. Atlee, S. Gnesi
Pages14-30
DOIs
Publication statusPublished - 2015
Event6th Workshop on Formal Methods and Analysis in SPL Engineering (FMSPLE 2015), April 11, 2015, London, UK - London, United Kingdom
Duration: 11 Apr 201511 Apr 2015
http://fmsple15.isti.cnr.it/

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume182
ISSN (Print)2075-2180

Workshop

Workshop6th Workshop on Formal Methods and Analysis in SPL Engineering (FMSPLE 2015), April 11, 2015, London, UK
Abbreviated titleFMSPLE 2015
Country/TerritoryUnited Kingdom
CityLondon
Period11/04/1511/04/15
Other
Internet address

Fingerprint

Dive into the research topics of 'Coherent branching feature bisimulation'. Together they form a unique fingerprint.

Cite this