Using FMC for Family-Based Analysis of Software Product Lines

We show how the FMC model checker can successfully be used to model and analyze behavioural variability in Soft-ware Product Lines. FMC accepts parameterized specifi-cations 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. CCS Concepts •General and reference → Verification; •Theory of computation→Verification by model checking; Modal and temporal logics; Process calculi; Operational semantics; •Software and its engineering → Model checking; Software product lines; Model-driven software engineer-ing