About

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 paper) showed substantial gains over individual product verification.

Modelling examples

A technical report with a number of example FTS models and comparisons to other approaches is available for download here. Some of the examples in the technical report are also included in the distributed FTS Haskell library.