Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., De Vink E. P. Software product line analysis with mCRL2. In: SPLat 2014 - First Workshop on Software Product Line Analysis Tools affiliated with the 18th International Software Product Line Conference (SPLC'14) (Florence, Italy, 16 September 2014). Proceedings, vol. 2 pp. 78 - 85. Stefania Gnesi, Alessandro Fantechi, Maurice ter Beek, Goetz Botterweck, Martin Becker (eds.). ACM, 2014.
The mCRL2 language and supporting software provide a state-of-the-art tool suite for the verification of distributed systems. In this paper, we present the general principles, extrapolated from [BDV14a,BDV14b], which make us believe that mCRL2 can also be used for behavioral variability analysis of product families. The mCRL2 data language allows to smoothly deal with feature sets and attributes, its process language is sufficiently rich to model feature selection, as well as product behavior based on an FTS-like semantics. Because of the feature-orientation, our modeling strategy allows a natural refactoring of the semantic model of a product family into a parallel composition of components that reflects coherent sets of features. This opens the way for dedicated abstraction and reduction techniques that strengthen the prospect of a scalable verification approach to software product lines. In this paper, we sketch how to model product families in mCRL2 and how to apply a modular verification method, preparing the ground to further assess the scalability of our approach, in particular regarding model checking.
URL: http://dl.acm.org/citation.cfm?doid=2647908.2655970
DOI: 10.1145/2647908.2655970
Subject Product families
Behavioral analysis
Modular verification
Model checking
D.2.2 Design Tools and Techniques
D.2.4 Software/Program Verification. Formal methods
D.2.4 Software/Program Verification. Model checking
D.2.4 Software/Program Verification. Validation
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