PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Belder T., Ter Beek M. H., De Vink E. P. Coherent branching feature bisimulation. In: FMSPLE'15 - 6th International Workshop on Formal Methods for Software Product Line Engineering (London, UK, 11 April 2015). Proceedings, pp. 14 - 30. J.M. Atlee, S. Gnesi (eds.). (Electronic Proceedings in Theoretical Computer Science, vol. 182). EPTCS, 2015.
 
 
Abstract
(English)
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.
URL: http://eptcs.web.cse.unsw.edu.au/paper.cgi?FMSPLE15.2
DOI: 10.4204/EPTCS.182.2
Subject Software Product Line Engineering
Feature Transition Systems (FTS)
Branching bisimulation
FTS minimization
D.2.4 Software/Program Verification. Formal Methods
D.2.4 Software/Program Verification. Model checking
F.3.1 Specifying and Verifying and Reasoning about Programs
F.3.2 Semantics of Programming Languages


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional