Aide a la validation par paraphrasage de specifications formelles b

Le developpement d'un logiciel passe generalement par plusieurs etapes, depuis la redaction du cahier des charges jusqu'a l'installation et le suivi du logiciel chez le client : c'est son cycle de vie (il existe plusieurs types de cycles de vie : en spirale, en x, en v, etc. ). Dans cette these, nous portons notre interet sur l'etape de specification dans le cycle de vie du logiciel, et plus precisement sur la validation de cette etape. Nous avons choisi d'etudier les specifications formelles ecrites dans le langage b. Notre etude de validation vient a la suite des aspects verification mis en uvre par les outils tels que l'atelier b. Nous pensons que la validation du logiciel, contrairement a la verification, ne peut pas se faire sans le client (celui qui a commande le logiciel). Dans la plupart des cas, ce dernier ne comprend pas le langage utilise par l'expert (informaticien) pour ecrire la specification. C'est pourquoi, pour permettre au client de comprendre la specification, afin de la valider ou de l'invalider, celle-ci doit etre paraphrasee par un texte en langage naturel. Dans cette these, nous proposons une demarche de generation d'un texte en francais a partir de la specification a valider. La demarche comprend trois etapes. La premiere consiste en une extraction des connaissances a partir de la specification b. Les connaissances extraites sont representees par des graphes conceptuels. Ces derniers sont transformes en squelettes de phrases lors de la deuxieme etape. La troisieme etape se resume en une generation de texte, appele paraphrase, a partir des squelettes de phrases. Ce texte peut ensuite etre soumis au client pour validation. Si la paraphrase n'est pas validee, l'expert doit alors revoir sa specification ou eventuellement redefinir les besoins avec le client. Afin de valider notre proposition, nous avons realise un prototype qui, a partir d'une specification b, genere un texte en francais. Ce prototype a ete lui-meme, en partie, formellement specifie en utilisant le langage b.