Vérification de Lignes de Produits Logiciels

Projet: Recherche

Détails du projet

Description

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.
AcronymeVLPL
statutFini
Les dates de début/date réelle1/01/111/01/13

mots-clés

  • verification de modeles
  • automates
  • verification de logiciel
  • lignes de produits logiciels
  • vérification de modèles
  • vérification de logiciel

Résultat de recherche

A methodology for formal analysis and verification of EAST-ADL models

Kang, E-Y., Enoiu, E. P., Marinescu, R., Seceleanu, C., Schobbens, P. Y. & Pettersson, P., 31 juil. 2013, Dans : Reliability Engineering and System Safety. 120, p. 127-138 12 p.

Résultats de recherche: Contribution à un journal/une revueArticle

  • Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking

    Classen, A., Cordy, M., Schobbens, P-Y., Heymans, P., Legay, A. & Raskin, J-F., 1 janv. 2013, Dans : IEEE Transactions on Software Engineering. 39, 8, p. 1069-1089 21 p.

    Résultats de recherche: Contribution à un journal/une revueArticle

  • Model checking adaptive software with featured transition systems

    Cordy, M., Classen, A., Heymans, P., Legay, A. & Schobbens, P., 1 janv. 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Principles, Models, and Techniques. Cámara, J., de Lemos, R., Ghezzi, C. & Lopes, A. (eds.). Heidelberg Dordrecht London New York: Springer, Vol 7740. p. 1-29 29 p. (Lecture Notes in Computer Science).

    Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceChapitre

    Accès ouvert
    File
  • 189 Téléchargements (Pure)