Paper Info
Title
Using FMC for family-based analysis of software product lines
Abstract
We show how the FMC model checker can successfully be used to model and analyze behavioural variability in Software Product Lines. FMC accepts parameterized specifications in a process-algebraic input language and allows the verification of properties of such models by means of efficient on-the-fly model checking. The properties can be expressed in a logic that allows to correlate the parameters of different actions within the same formula. We show how this feature can be used to tailor formulas to the verification of only a specific subset of products of a Software Product Line, thus allowing for scalable family-based analyses with FMC. We present a proof-of-concept that shows the application of FMC to an illustrative Featured Transition System from the literature.
Year
DOI
Venue
2015
10.1145/2791060.2791118
Software Product Lines
Field
DocType
Citations 
Transition system,Parameterized complexity,Model transformation,Model checking,Systems engineering,Computer science,Software,Software product line,Process calculus,Scalability
Conference
4
PageRank 
References 
Authors
0.40
28
4
Name
Order
Citations
PageRank
Maurice H. ter Beek171862.08
Alessandro Fantechi21199103.40
Stefania Gnesi31475120.93
Franco Mazzanti427221.69