La spécification des systèmes temps réel pose le problème de l'expression du temps et des contraintes temporelles pour lesquels nous proposons dans ce mémoire, une nouvelle représentation. Cette représentation est basée sur l'hypothèse que l'écoulement du temps est modélisé par l'occurrence d'un événement spécifique. Cette conception nous permet de considérer les contraintes temporelles comme des propriétés de séquences d'événements observables. En relation avec une notation simple, basée sur la notion de grammaire, les propriétés temporelles deviennent des propriétés syntaxiques. Ces considérations nous ont amenés à proposer une nouvelle méthode d'analyse des contraintes temporelles qui a pour objet de vérifier que toutes les contraintes temporelles d'un cahier des charges ont bien été prises en compte dans l'étape de spécification. Pour réaliser cette vérification, on élabore un analyseur de traces temporisées dont la construction se fait en deux étapes. On extrait d'abord les contraintes temporelles en suivant une décomposition structurée. Cette décomposition permet d'identifier un ensemble d'opérateurs (périodique, sporadique, de disjonction ou de conjonction) liant les contraintes temporelles. On exprime ensuite ces contraintes, sous la forme de grammaires «types». La seconde étape est la recomposition de ces grammaires, par l'ensemble des opérateurs précédemment identifiés. Pour cela, on a redéfini chacun de ces opérateurs pour qu'ils puissent s'appliquer sur des grammaires. Le résultat final de cette recomposition produit une grammaire globale qui constitue un analyseur syntaxique, capable de vérifier si une trace temporisée vérifie ou non, toutes les contraintes temporelles du cahier des charges.