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éponse | 2011 |
---|
langue originale | Français |
---|
L'institution diplômante | |
---|
Superviseur | Patrick Heymans (Promoteur) |
---|
Traduction de TVL en SMT-LIBv2
Vanderveken, T. (Auteur). 2011
Student thesis: Master types › Master en sciences informatiques