Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Fantechi A., Gnesi S., Mazzanti F. Using FMC for family-based analysis of Software product lines. In: SPLC'15 - 19th International Software Product Line Conference (Nashville, TN, USA, 20-24 July 2015). Proceedings, pp. 432 - 439. ACM, 2015.
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.
DOI: http://dx.doi.org/10.1145/2791060.2791118
Subject Variability
Featured Transition Systems
Process algebra
Model transformation
D.2.4 Software/Program Verification. Formal methods
D.2.4 Software/Program Verification. Model checking
D.2.13 Reusable Software. Domain engineering
F.3.2 Semantics of Programming Languages. Process models
F.4.1 Mathematical Logic. Modal logic
F.4.1 Mathematical Logic. Temporal logic

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