Abstract FR:

La production automatique de code non seulement efficace mais aussi prouve correct par rapport a sa specification est un probleme interessant car il permet de tendre vers un des buts les plus recherches : la conception zero defaut. De plus, de nombreux progres dans le domaine de la verification formelle ont ete realises ces dix dernieres annees et les industriels commencent a s'y interesser. Cette these s'inscrit dans ce cadre pour des processeurs dedies au traitement du signal, les dsps de la famille tms320 de texas instruments. Le developpement d'applications sur ces processeurs se fait soit en utilisant le langage c comme langage de haut niveau, soit directement en langage d'assemblage. Les compilateurs c, bien qu'optimises, ne permettent pas en general d'atteindre, lorsque la cible est un dsp en virgule fixe, un niveau de performance suffisant. De plus une programmation en langage d'assemblage n'est rentable que pour des applications stables et perennes. En fait, on peut considerer qu'il manque des langages de haut niveau permettant une programmation rapide et efficace des processeurs dsp. Nous avons alors defini un langage de programmation declaratif d'un niveau d'abstraction raisonnablement eleve (sml) destine a la specification de systemes dynamiques que sont les applications de traitement du signal. Ce langage sml se place, en fait a un niveau d'abstraction inferieur a celui des langages plus generalistes tels que signal, lustre ou des langages a descriptions graphiques dont il pourrait servir de langage intermediaire. Nous avons aussi defini une machine virtuelle intermediaire smam, non seulement pour palier les limitations d'une implementation fortement dependante du dsp cible mais aussi pour rendre la preuve plus facile en introduisant un niveau intermediaire d'abstraction entre la specification et le processeur dsp. Notre contribution a ce niveau a ete de produire du code dsp plus efficace que celui produit par un compilateur c principalement utilise aujourd'hui. De plus nous nous sommes interesses a une implementation prouvee de programmes sml sur les processeurs dsp ce qui revient a verifier formellement que le compilateur, produisant du code assembleur a partir d'un programme de specification sml, est correct.