Modelling and model checking variability-intensive systems

Résumé

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.

la date de réponse	3 oct. 2011
langue originale	Anglais
L'institution diplômante	Universite de Namur
Superviseur	Patrick Heymans (Promoteur), Pierre Yves Schobbens (Copromoteur), Jean-Marie Jacquet (Jury), Naji Habra (Jury), Charles PECHEUR (Jury), Bashar Nuseibeh (Jury) & Joost-Pieter KATOEN (Jury)