|
 
|
[Pha17a] Development of Correct-by-Construction Software using Product Lines
Mémoire de Thèse : Soutenue le: 16 November 2017,Mots clés: Développement correct-par-construction, ligne de produits logiciels, variablilité, spécification formelle, preuve formelle, FoCaLiZe, Zenon
Résumé:
Aujourd’hui, la diversité des logiciels pose des difficultés à de nombreuses entreprises et organisations. Alors que l’ingénierie des lignes de produits logiciels est considérée comme une solution possible et utilisée dans de nombreux domaines depuis des décennies, la problématique du développement de lignes de produits corrects par construction est toujours d’actualité. Cette thèse commence par une présentation de quelques techniques existantes appliquées pour développer et garantir la correction des lignes de produits logiciels. Nous proposons une solution basée sur la conception et la mise en œuvre d’un langage FFML (Formal Feature Module Language) inspiré du langage FoCaLiZe et fournissant des mécanismes pour exprimer la réutilisation et la variabilité. Ce langage permet de spécifier, implanter une fonctionnalité et prouver sa correction en donnant des indications au prouveur automatique de théorèmes Zenon. Nous développons un compilateur de FFML en FoCaLiZe. Nous fournissons également un mécanisme de composition qui, appliqué à une configuration valide fournie par l’utilisateur, produit automatiquement un produit final correct-par-construction, ce qui signifie que le code produit est correct par rapport à ses spécifications, elles-aussi obtenues par composition des spécifications des caractéristiques impliquées dans la configuration de l’utilisateur. Enfin, nous évaluons notre méthodologie en construisant une ligne de produits logiciels pour le poker.
BibTeX
| @phdthesis { | |||
| Pha17a, | |||
| title | = | "{Development of Correct-by-Construction Software using Product Lines}", | |
| author | = | "T. Pham ", | |
| year | = | 2017, | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| } |
