Software Product Line Engineering (SPLE) is a software engineering methodology aimed at developing, in a cost-effective and time-efficient manner, a family of software-intensive highly configurable systems by systematic reuse. Individual products (or variants) share an overall reference variability model of the family, but they differ with respect to specific features, which are user-visible increments in functionality. The explicit introduction and management of feature-based variability in the software development cycle causes complexity in the modelling and analysis of SPLs, because the number of possible individual products typically grows exponentially with the number of features. An important example concerns behavioural validation, i.e., guaranteeing that each product of the SPL satisfies a series of behavioural requirements. Variants of this problem include computing a set of products that do not satisfy the requirements plus a justification. A common approach to assess these requirements consists of building the system and testing it. However, if the system fails to meet the requirements, costly interactions are needed to improve it. Recent research has focussed on lifting successful formal specification languages and formal verification techniques known from single system engineering to product line engineering or highly configurable systems in general.
In this lecture, after a general introduction to SPLE, we present a number of modelling and analysis frameworks that were introduced for the specification and verification of variability in behavioural models of SPLs. These range from variants of Modal Transition Systems (MTSs) and Featured Transitions Systems (FTSs) and their dedicated family-based model checkers VMC and SNIP/ProVeLines to QFLan, a quantitative modelling and verification environment offering a probabilistic feature-oriented language and statistical model checking.
Much of what I present is based on joint work with colleagues from the Formal Methods and Tools group in Pisa and with Axel Legay, Alberto Lluch Lafuente and Andrea Vandin.
In an accompanying lecture, Erik de Vink will focus on a feature mu-calculus over FTSs that allows family-based model checking with mCRL2.