|
 
|
[DLP16] Vers un développement formel non incrémental
Conférence Nationale avec comité de lecture : AFADL'2016, June 2016, pp.106-113, Besançon, France,Mots clés: Ligne de produits, logiciels corrects par construction, FoCaLiZe
Résumé:
Modularité, généricité, héritage sont des mécanismes qui facilitent le développement
et la vérification formelle de logiciels corrects par construction en permettant
de réutiliser des spécifications, du code et/ou des preuves. Cependant les
lignes de produits exploitent d’autres techniques de réutilisation ou de modification
graduelle. Les méthodes formelles permettant la production de code correct
par construction (en B ou FoCaLiZe par exemple) ne sont pas bien adaptées à la
variabilité telle qu’elle apparaît dans les lignes de produits. Nous proposons d’approcher
ce problème par la définition d’un langage formel, GFML, proche de la
variabilité mise en oeuvre dans les lignes de produits permettant de spécifier, implanter
et prouver. Ce langage est compilé vers un formalisme existant, ici FoCa-
LiZe. Cet article illustre par l’exemple une des constructions offertes par GFML
ainsi que sa traduction en FoCaLiZe.
Commentaires:
In //hal.inria.fr/hal-01326694/file/AFADL2016.pdf
BibTeX
| @inproceedings { | |||
| DLP16, | |||
| title | = | "{Vers un développement formel non incrémental}", | |
| author | = | " C. Dubois and N. Levy and T. Pham ", | |
| booktitle | = | "{AFADL'2016}", | |
| year | = | 2016, | |
| month | = | "June", | |
| pages | = | "106-113", | |
| address | = | "Besançon, France", | |
| note | = | "{In //hal.inria.fr/hal-01326694/file/AFADL2016.pdf}", | |
| } | |||
