Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour la sécurité : ils en contrôlent l'exécution afin que celles-ci se comportent de manière sûre dans le contexte d'un environnement dont l'évolution peut être imprévisible. Un STR n'a d'autre alternative que de s'adapter `a son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier. Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté à la description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelques tâches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe. En premier lieu, la modélisation efficace d'une gamme étendue de politiques d'ordonnancements se heurte à l'incapacité des RdPT à imposer un ordre d'apparition à des évènements concurrents survenant au même instant. D'autre part, les STR ont une nette tendance à être constitués de caract éristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guère adaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deux problèmes, nous proposons dans cette thèse Cifre - en partenariat entre Airbus et le Laas-Cnrs - d'étendre les RdPT à l'aide de deux nouvelles relations, les relations d'inhibition et de permission, permettant de spécifier de manière plus fine les contraintes de temps. Afin de cerner un périmètre clair d'adéquation de cette nouvelle extension à la modélisation des systèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs : déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporels à inhibitions/permissions et fournir un langage simple à la communauté temps réel dont la vérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L'explorateur d'espace d'états de la boite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola.

Ce travail porte sur la specification et la verification des systemes temps reel. Nous presentons une algebre de processus temporises ATP, qui permet de decrire de tels systemes en utilisant divers operateurs temporels. Sa semantique operationnelle est basee sur l'hypothese de synchronisme des langages synchrones. Elle definit les modeles des processus comme des systemes de transitions etiquetees, dans lesquels l'evolution discrete du temps est denotee par une etiquette particuliere. Une axiomatisation complete offre la possibilite de comparer deux termes de l'algebre modulo l'equivalence forte sans construire leurs modeles. Nous generalisons ensuite la semantique d'ATP a des domaines temporels quelconques, en particulier des domaines denses. Nous montrons qu'une propriete de surete est satisfaite par un processus pour tout domaine temporel discret si elle l'est pour un domaine dense. Nous etudions dans un deuxieme temps les graphes temporises, qui sont des automates etendus par des compteurs de temps. Nous presentons une methode de traduction d'ATP vers les graphes temporises qui preserve la semantique des processus. Le graphe obtenu presente l'interet d'etre de taille independante des valeurs des delais apparaissant dans la description, car les contraintes temporelles y sont exprimees symboliquement. Finalement, nous decrivons un algorithme de verification de proprietes sur les graphes temporises. Il consiste a evaluer symboliquement des formules d'une logique temporelle temps reel en evitant l'explosion combinatoire du nombre d'etats des modeles de bas niveau causee par les valeurs des delais. Nous obtenons ainsi les principes theoriques d'un outil de description et de verification de systemes temps reel.