Abstract FR:

Le sujet de thèse traite la problématique liée à la validation temporelle d'une application multitâche temps réel ayant comme support les noyaux temps réel. Une étude comparative a été établie qui consistait à comparer deux formalismes très connus dans le domaine de la validation temporelle. Il s'agit des réseaux de Petri et les automates temporisés. Nous avons conclu que les deux formalismes restent équivalents sur beaucoup de formes. L'avantage de la théorie des automates que nous avons choisi consistait autour de l'existence d'outils de simulation et de vérification des propriétés temporelles. Par ailleurs nous avons choisi la notation IF basée sur les automates temporisés communicants une variante des automates temporisés comme langage de base pour exprimer une application multitâche temps réel, les objets du noyau temps réel, l'environnement extérieur. Par conséquent la première contribution de cette thèse d'une part, consistait à formaliser des parties des noyaux temps réel. Nous avons pris comme exemple de noyau temps réel VxWorks de Wind River Systems. Nous avons pu dégager une plate forme minimale décrite à l'aide de la notation IF basée sur les automates temporisés communicants. Cette plate forme est constituée par la gestion des tâches, les moyens de communication/synchronisation, la gestion des interruptions et du temps. D'autre part, nous avons modélisé les mécanismes qui régissent un ordonnnanceur préemptif à priorité fixe. L'architecture matérielle est prise en compte à travers la modélisation des durées d'exécution des fonctions. Ces restrictions ont été prises lors de l'application de ces techniques au cas de VxWorks. Par ailleurs nous avons proposé des modèles qui permettent de représenter l'environnement extérieur. La deuxième contribution de cette thèse consistait à valider temporellement une application multitâche temps réel en se basant la technique de simulation du package IF afin de mener des vérifications des propriétés de sûreté (par exemple la non utilisation d'objets non crées), des propriétés d'équité ou d'absence de blocages et enfin la vérification des pires cas d'exécution.