Vérification de Lignes de Produits Logiciels

La plupart des logiciels actuels se déclinent en de nombreuses variantes (logiciels pour GSM, voitures, services de télécommunication etc.). Nous les appelons des Lignes de Produits Logiciels (LPL). Le développement de LPL permet en principe une réutilisation massive de composants, pouvant engendrer une réduction importante des coûts et des délais de mise sur le marché. Cependant, ce développement présente aussi un risque de perte de maîtrise des nombreuses variantes à gérer en parallèle.
La difficulté de ce problème résulte (i) du grand nombre de variantes possibles, exponentiel par rapport au nombre de caractéristiques optionnelles (appelées "features"), (ii) de la complexité de ces logiciels, qui amène à des interactions difficiles à prévoir, (iii) des conséquences importantes des défaillances.
Nous nous proposons d'approcher ce problème par le développement d'un langage de spécification et des techniques de vérification formelles. Le but d'une technique de vérification formelle est de garantir la fiabilité du logiciel. Pour ce faire, on utilise des modèles et des techniques mathématiques qui permettent de s'assurer que tous les comportements d'un logiciel satisfont un ensemble de propriétés données dans une logique temporelle. Dans une série de travaux récents, nous avons proposé un modèle, que nous appelons "Featured Transition Systems (FTS)", qui permet de décrire de façon concise les comportements de toutes les variantes d'un produit. Ces variantes doivent pouvoir être gérées en parallèle. En plus de notre langage, nous avons aussi développé une logique temporelle permettant de décrire les propriétés d'une LPL. Cette logique permet de décrire explicitement les propriétés que les variantes doivent satisfaire (par exemple, le système de contrôle n'est jamais bloqué, le système finit toujours par rendre la main à l'utilisateur, etc.). En nous basant sur le langage FTS, nous avons mis au point une série d'algorithmes de vérification basés sur le principe du "model-checking" afin de vérifier ces propriétés. Etant donné une description sous forme de FTS et une propriété, nos algorithmes permettent de déterminer quelles sont les variantes qui la satisfont et quelles sont les variantes qui ne la satisfont pas. Nos algorithmes, implémentés au sein d'un prototype, se sont montrés efficaces sur des cas d'étude académiques.
Jusqu'à présent, les fondements théoriques du langage, de la logique et des algorithmes ont été au centre de nos travaux. L'objectif du projet est de continuer à développer nos algorithmes et nos techniques de vérifications.
Plus précisément, il s'agira (i) de terminer les travaux théoriques en cours et d'intégrer les différents algorithmes au sein d'une même structure, (ii) de développer un outil et un langage de description pratique et utilisable par les développeurs de produit, et (iii) d'évaluer notre approche par une étude de cas industrielle.