|
 
|
[PDL17] Une ligne de produits corrects par construction
Conférence Nationale avec comité de lecture : AFADL 2017, June 2017, pp.7 p, Montpellier, France,Mots clés: Lignes de produits logiciels, logiciels corrects par construction, FoCaLiZe
Résumé:
L’ingénierie des lignes de produits logiciels met l’accent sur la gestion
de la variabilité et la réutilisation. Dans cet article, nous complétons cette
approche avec la recherche de garanties de correction sur les produits issus
d’une ligne de produits. Nous proposons une méthode permettant de produire
des produits corrects par construction à partir d’une ligne de produits. Cette
méthode s’appuie sur un langage, FFML, inspiré de FoCaLiZe et incorporant
des mécanismes pour exprimer la variabilité, et deux outils : un compilateur
vers FoCaLiZe et un composeur. Le composeur permet de générer automatiquement
des produits corrects par construction à partir d’une configuration
valide. Les outils de FoCaLiZe permettent de vérifier les preuves de correction
et de générer du code exécutable OCaml. La méthode est illustrée dans
cet article sur un exemple simple de ligne de produits.
BibTeX
| @inproceedings { | |||
| PDL17, | |||
| title | = | "{Une ligne de produits corrects par construction}", | |
| author | = | " T. Pham and C. Dubois and N. Levy ", | |
| booktitle | = | "{AFADL 2017}", | |
| year | = | 2017, | |
| month | = | "June", | |
| pages | = | "7 p", | |
| address | = | "Montpellier, France", | |
| } | |||
