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.
Using FMC for family-based analysis of Software product lines
Ter Beek MH;Fantechi A;
2015-01-01
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.File | Dimensione | Formato | |
---|---|---|---|
prod_333021-doc_103257.pdf
solo utenti autorizzati
Descrizione: Using FMC for family-based analysis of Software product lines
Tipologia:
Versione Editoriale (PDF)
Dimensione
847.54 kB
Formato
Adobe PDF
|
847.54 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
prod_333021-doc_159175.pdf
accesso aperto
Descrizione: Using FMC for family-based analysis of Software product lines
Tipologia:
Versione Editoriale (PDF)
Dimensione
359.67 kB
Formato
Adobe PDF
|
359.67 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.