Développement formel de systèmes temps réel à l\u27aide de SDL et IF : compilation pour systèmes temps réel

Un système temps réel est un système qui interagit avec un environnement physique en remplissant souvent des missions critiques (une faute du système peut avoir des conséquences graves). Il sera dit correct s\u27il possède les bonnes fonctionnalités réalisées à temps (contraintes temporelles imposées par l\u27environnement ou par l\u27utilisateur). La validation fonctionnelle et temporelle de ces systèmes est une nécessité forte (fournisse des résultats fiables). Dans le cadre des implémentations à base d\u27exécutifs multitâche temps réel, le travail présenté dans cette thèse tente d\u27apporter une approche complète formelle de la suite spécification, conception et implémentation. Dans ce cadre, il porte aussi un intérêt particulier à une méthode de validation de la transformation entre le modèle de contraintes et le modèle d\u27exécution. Nous formalisons plus particulièrement des phases de spécification et la conception en utilisant le langage formel SDL. Ensuite, nous précisons explicitement les contraintes temps réel à nos modèles en utilisant le langage IF. Enfin, nous montrons formellement comment la correction du développement d\u27une application est prouvée