Model Checking for the Masses

The model-checking problem for software product lines is harder than for single systems. Indeed, one has to verify all the software variants of a product line, whose number grows exponentially in the number of their differences. Techniques intended for single systems are inefficient in this case, for these can only be applied to all products separately. Variability-aware modelling formalisms and algorithms were designed as a more appropriate answer to that problem. Their strength lies in their ability to check a behaviour common to several products only once, which leads to substantial performance gains. Although they constitute a major step toward the efficient verification of product lines, these techniques are not yet mature enough to truly achieve this objective. They still lack optimisations to verify large models, the expressiveness to represent complex forms of variable behaviour, as well as usable languages and tools required for industrial transfer. This thesis aims at improving product-line model checking in order to provide formalisms, algorithms, and tools that together hold the potential to verify real-world software product lines. We first study the state-of-the-art model-checking approaches for software product lines. We compare them in terms of available formalisms and algorithms, and we determine that the approach based on Featured Transition Systems (FTS) is the most suitable to act as a basis for the design of novel techniques. We then extend its theory along two axes: efficiency and expressiveness. For the former, we propose abstraction methods that can reduce the size of the model to check while maintaining correctness and completeness; they consist of extensions of single-system abstraction techniques applied to FTS, and of new techniques that abstract away from their variability. As for expressiveness, on the one hand we propose featured timed automata as a combination of FTS and real-time behaviour. On the other hand, we analyse how to support in FTS complex forms of variability such as numeric features and multi-features. We implemented our theoretical results into a new model-checking tool named ProVeLines. As all our extensions are based on FTS, they share many commonalities. ProVeLines was therefore designed as a product line whose each variant implements a distinct combination of verification formalisms and algorithms. Finally, we show that the principles we designed for product-line model checking can also be applied to other formal methods, namely the verification of adaptive systems and the synthesis of controllers for product lines.