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. |

Abstract (English) |
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 Features 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 |

1) Download Document PDF |

Open access Restricted Private