Abstract FR:

Lorsque la maintenance est negligee pendant le developpement du logiciel, elle fait souvent l'objet d'une pratique empirique, couteuse et source de deterioration du logiciel. Pour les nouveaux logiciels, l'integration de specifications formelles dans le processus de developpement fournit un cadre pour une maintenance plus performante. Pour les logiciels existants, une integration a posteriori peut se faire via une phase de retro-ingenierie qui consiste a extraire des descriptions abstraites du logiciel a partir de ses sources. Dans cette these, nous proposons une methode de retro-ingenierie qui fournit des descriptions de la structure et des fonctionnalites d'un logiciel fortran sous la forme de specifications algebriques. Pour extraire la signature, nous utilisons des techniques d'analyse de flots de donnees et de controle et nous traitons de problemes lies a l'absence de declaration de type en fortran, a la manipulation de pointeurs et a l'utilisation incoherente de variables globales et locales dans le code. Pour extraire les axiomes, nous utilisons des techniques de decoupage de programmes et de reconnaissance de schemas de code et nous traitons de problemes lies a l'imbrication de boucles et de selections et a l'utilisation de goto. Par ailleurs, nous avons concu plusieurs processus permettant d'automatiser les etapes de la methode qui pouvaient l'etre. Enfin, il est important de noter que la methode proposee permet aussi de detecter des defauts dans le code : faux parametres, code mort, cycles, code redondant, decalages entre le code et la documentation.