Paper Info
Title
Software product line analysis with mCRL2
Abstract
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 [7,8], 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.
Year
DOI
Venue
2014
10.1145/2647908.2655970
SPLC Workshops
Keywords
Field
DocType
design,experimentation,behavioral analysis,variability,model checking,verification,domain engineering,formal methods,product families,modular verification,validation
Programming language,Model checking,Systems engineering,Computer science,Theoretical computer science,Software,Feature model,Software product line,Code refactoring,Semantic data model,Software engineering,Software verification,Scalability
Conference
Citations 
PageRank 
References 
5
0.41
45
Authors
2
Name
Order
Citations
PageRank
Maurice H. ter Beek171862.08
Erik P. de Vink237428.76