PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., De Vink E. P., Willemse T. A. Towards a feature mu-calculus targeting SPL verification. In: FMSPLE 2016 - Formal Methods and Analysis in Software Product Line Engineering (Eindhoven, The Netherlands, 3 April 2016). Proceedings, vol. 206 pp. 61 - 75. Julia Rubin, Thomas Thüm (eds.). (Electronic Proceedings in Theoretical Computer Science, vol. 206). EPTCS, 2016.
 
 
Abstract
(English)
The modal mu-calculus mu-L is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the mu-calculus, mu-Lf and mu-Lf', for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific products and subfamilies. We provide semantics for mu-Lf and mu-Lf' and relate the two new mu-calculi and mu-L to each other. Next, we focus on the analysis of SPL behavior and show how our formalism can be applied for product-based verification with mu-Lf as well as family-based verification with mu-Lf'. We illustrate by means of a toy example how properties can be model checked, exploiting an embedding of mu-Lf' into the mu-calculus with data.
URL: http://eptcs.web.cse.unsw.edu.au/paper.cgi?FMSPLE2016.6
DOI: 10.4204/EPTCS.206.6
Subject Family-based model checking
mu-calculus with features
Behavioral SPL models
Featured Transition Systems
D.2.4 Software/Program Verification. Formal methods
D.2.4 Software/Program Verification. Model checking
D.2.13 Reusable Software. Domain engineering


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