Modelling and Model Checking Variability-Intensive Systems

(eng) The premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. However, in the case of safety critical systems, only a tiny fraction of the possible systems are generally offered to customers. One reason for this is that current quality assurance techniques used in the development of these systems, such as model checking, are designed for systems with no variability. In consequence, they are costly to apply to the whole system family. More specifically, when differences between systems are expressed in terms of features, the number of possible systems in a family is exponential in the number of features. Two major challenges for quality assurance techniques are thus scalable models and efficient algorithms. We address these challenges for a specific quality assurance technique: model checking. The proposed model checking approach is based on Featured Transition Systems (FTS), a novel formalism introduced in this thesis. FTS are a compact mathematical model for representing the behaviours of a variability-intensive system. Basically, they are transition systems in which the presence of a transition depends on the features of the system. We define and study model checking algorithms that allow to verify FTS against temporal properties. They either prove that all systems of the family satisfy the property, or identify those that do not. Properties can be specified in feature LTL and feature CTL, extensions of the well known linear and branching time temporal logics. In addition to the mathematical foundation, we discuss two implementations of FTS that can be used by non-experts. A first uses a symbolic representation of the state space and is implemented as part of the NuSMV model checker. The second, SNIP, uses a semi-symbolic on-the-fly algorithm. SNIP comes with an intuitive specification language based on Promela. Finally, we propose theoretical and empirical evaluations of our results. The baseline for our empirical evaluation is the application of classical model checking algorithms to each system of the family. Experiments conducted with both model checkers show that our algorithms can achieve order-of-magnitude speedups.

(fre) L'ingénierie des lignes de produits logiciels est un paradigme d'ingénierie du logiciel dont le but est de permettre le développement efficace de grandes familles de logiciels. Cependant, dans le cas des systèmes critiques, peu de membres d'une famille de produits sont généralement vendus aux clients. En effet, les techniques d'assurance qualité utilisées dans le développement de ce type de systèmes, telles que le model checking, ne peuvent traiter que des systèmes sans variabilité. En conséquence, il est très coûteux d'appliquer ces techniques à tous les systèmes d'une même famille. Si les différences entres les systèmes sont exprimées en terme de features, le nombre de systèmes possibles est exponentiel en fonction du nombre de features. Deux défis importants pour les techniques d'assurance qualité sont donc le développement de modèles et d'algorithmes qui passent à l'échelle. Nous traitons ces défis pour une technique spécifique: le model checking. La technique de model checking proposée est basée sur les Featured Transition Systems (FTS), un nouveau formalisme introduit dans cette thèse. Les FTS sont un modèle mathématique pour représenter le comportement d'une famille de systèmes de façon compacte. Un FTS est essentiellement un système de transitions dans lequel la présence d'une transition dépend des features. Nous proposons et étudions des algorithmes permettant de vérifier des propriétés temporelles sur des FTS. Ces algorithmes peuvent prouver que tous les systèmes d'une famille satisfont une propriété donnée, ou bien ils identifient ceux qui ne le font pas. Pour spécifier les propriétés, nous proposons feature LTL and feature CTL, des extensions des deux logiques temporelles classiques. En plus des fondements mathématiques, nous décrivons deux implémentations des FTS utilisables par des non-experts. La première utilise une représentation symbolique de l'espace d'états et a été implémentée au sein du model checker NuSMV. La deuxième, appelée SNIP, utilise un algorithme semi-symbolique à la volée. Le langage de modélisation de SNIP est basé sur le langage Promela. Enfin, nous discutons une évaluation théorique et empirique de nos résultats. Le cas de base utilisé pour l'évaluation empirique est l'application d'un algorithme de model checking classique à chaque produit. Les expériences conduites avec les deux outils montrent que nos algorithmes peuvent atteindre des gains en vitesse de plusieurs ordres de grandeur par rapport au cas de base.