Abstract FR:

Cette these s'inscrit dans le cadre du developpement du langage signal dont les objectifs sont la specification et la mise en uvre d'applications temps-reel critiques. Nos travaux ont concerne l'extension du compilateur de signal qui est un outil formel pour la verification des contraintes de synchronisation d'horloges en signal. De maniere plus generale, notre etude se situe dans un contexte de conception conjointe de systemes mixtes materiel/logiciel (codesign) pour laquelle l'environnement de programmation de signal s'est prouve tres adapte. Dans ce contexte, nous avons constate que les langages signal et alpha possedent des proprietes complementaires concernant la programmation de traitements numeriques importants relies par du controle. Alpha est un langage fonctionnel pour la specification et l'implementation d'algorithmes reguliers, tandis que l'apport de signal se manifeste dans le domaine du controle. L'interfacage des deux langages a releve le probleme du raffinement des specifications mixtes et leur validation. Les transformations de specifications ont induit des transformations affines sur les horloges signal et la necessite de mettre en place un calcul formel sur les synchronisations des horloges transformees. Le nouveau calcul formel mis en place est base sur un ensemble de regles de synchronisabilite deduites a partir des proprietes des transformations affines. Nous avons retrouve des conditions de synchronisabilite basees sur un calcul d'entiers qui nous ont permis d'etendre les capacites de preuve formelle du compilateur de signal. Nous avons valide le calcul de synchronisabilite propose et les concepts lies a la conception conjointe avec signal et alpha a travers une application du domaine de codage d'images video.