FTS, featured transition systems, are a formalism designed to describe the combined behaviour of a whole system family. FTS are transition systems in which transitions are labelled with features of a software product line (in addition to being labelled with actions). This allows to model very detailed behavioural variations of the product line. In addition, features as treated as first-class abstractions, resulting in a clear separation of concerns.
FTS come with a tool-supported model checking approach that allows to verify FTS against LTL and CTL properties. The purpose of the approach is to verify all the products of a family at once and to pinpoint the products that violate properties. An empirical evaluation conducted for the LTL algorithms (ICSE 2010 paper) showed substantial gains over individual product verification. In our paper at ICSE 2011, we show that this approach extends to symbolic model checking of CTL properties, with a tool based on NuSMV.
A technical report with a number of example FTS models and comparisons to other approaches is available for download here.