On Featured Transition Systems

International audienceSoftware Product Lines (SPLs) are families of similar softwareproducts built from a common set of features. As the number ofproducts of an SPL is potentially exponential in the number of its features,analysing SPLs is harder than for single software. In this invitedpaper, we synthesise six years of efforts in alleviating SPL verificationand testing issues. To this end, we introduced Featured Transition Systems(FTS) as a compact behavioural model for SPLs. Based on this formalism,we designed verification algorithms and tools allowing to checktemporal properties on FTS, thereby assessing the correct behaviour ofall the SPL products. We also used FTS to define test coverage andgeneration techniques for model-driven SPLs. We also successfully employedthe formalism in order to foster mutation analysis. We concludewith future directions on the development of FTS for SPL analysis