Traduction de TVL en SMT-LIBv2

  • Thibault Vanderveken

Student thesis: Master typesMaster en sciences informatiques

Résumé

Les feature models jouent un rôle clé dans la capture des similitudes et de la variablité des lignes de produits. Depuis la notation originale FODA, les feature models ont connu plusieurs extensions et notations dont TVL, qui combine la plupart des extensions existantes, ce qui lui confère une grande expressivité. Depuis des années, les automatisations sur les feature models comme la vérification de la satisfiabilité font l'objet de recherche et l'on a déjà proposé de nombreuses solutions. Dans ce document, on fournit une solution pour vérifier la consistance de feature model en TVL. Pour ce faire, on a utilisé SMT-LIBv2 qui définit un langage commun d'entrée et de sortie pour les solveurs SMT. Il est également question des différentes possiblités de traduction ainsi que des limites de l'approche.
la date de réponse2011
langue originaleFrançais
L'institution diplômante
  • Universite de Namur
SuperviseurPatrick Heymans (Promoteur)

Contient cette citation

'