Vers un développement formel non incrémental

Modularite, genericite, heritage sont des mecanismes qui facilitent le developpement et la verification formelle de logiciels corrects par construction en permettant de reutiliser des specifications, du code et/ou des preuves. Cependant les lignes de produits exploitent d'autres techniques de reutilisation ou de modification graduelle. Les methodes formelles permettant la production de code correct par construction (en B ou FoCaLiZe par exemple) ne sont pas bien adaptees a la variabilite telle qu'elle apparait dans les lignes de produits. Nous proposons d'approcher ce probleme par la definition d'un langage formel, GFML, proche de la variabilite mise en oeuvre dans les lignes de produits permettant de specifier, implanter et prouver. Ce langage est compile vers un formalisme existant, ici FoCaLiZe. Cet article illustre par l'exemple une des constructions offertes par GFML ainsi que sa traduction en FoCaLiZe