Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.

Ce travail propose une méthode pour l'analyse de systèmes temps-reél. <br />Cette méthode est basée sur la compilation des spécifications<br />vers des graphes temporisés, à partir desquels il est possible<br />de vérifier des propriétés et de générer du code exécutable.<br /><br />Les graphes temporisés sont des automates étendus avec des<br />variables, appelées horloges, qui permettent de décrire les<br />contraintes temporelles. <br /><br />Un algorithme de compilation est développé pour l'algèbre<br />de processus temporisés ATP, qui est une extension des <br />algèbres de processus avec des opérateurs temporels comme <br />le ``timeout'' et le ``watchdog''. L'intérêt de l'algorithme est <br />que la taille du graphe obtenu est indépendante des valeurs <br />des paramètres des opérateurs temporels.<br /><br />Les propriétés temps-reél sur les graphes temporisés sont <br />décrites par des formules de la logique TCTL. <br />Il est montré que les opérateurs temporels<br />de TCTL s'expriment en termes de points fixes à l'aide d'un <br />opérateur ``d'état suivant'' défini de façon appropriée.<br />De plus, ce travail propose un algorithme de vérification qui<br />consiste à évaluer symboliquement l'ensemble caractéristique<br />d'une formule comme une disjonction de contraintes linéaires<br />sur les horloges.<br /><br />Les algorithmes de compilation et de vérification développés <br />ont été implémentés dans l'outil KRONOS, <br />utilisé pour analyser des applications temps-reél <br />significatives. Les résultats obtenus confirment l'intérêt<br />pratique de l'approche proposée.

Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles. / This PhD thesis proposes the theoretical foundations of a new formal tool for symbolic verification of finite models. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs).In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs).First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures.Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round RobinMutex protocols,... ) our tool is not only better than other rewriting tools such as Timbuk, Maude or TOM, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).