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.

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).

Cette thèse présente des méthodes et des algorithmes pour l'évaluation de performance de systèmes à grand espace d'états décrits par des formalismes de haut niveau. Parmi les différents formalismes de haut niveau normalement utilisés, nous nous sommes intéressés au formalisme des Réseaux d'Automates Stochastiques (SAN). Le formalisme SAN se caractérise par la modélisation de systèmes complexes, où un système est représenté par la composition de sous-systèmes (automates) qui interagissent entre eux. Cette interaction se réalise par l'occurrence des événements synchronisants ou des taux fonctionnels. Lorsqu'on calcule l'espace d'états atteignables de systèmes complexes, le principal problème qui surgit est l'explosion combinatoire de l'espace d'états du modèle. Dans la première partie de cette thèse, nous proposons des méthodes pour la génération de l'espace d'états atteignables de modèles compositionnels qui utilisent des taux fonctionnels. Nous utilisons les Diagrammes de Décision Multi-valués (MDD) pour représenter et manipuler les espaces d'états et le formalisme SAN pour la modélisation de systèmes. Un MDD est une structure de donnée arborescente qui permet de représenter et de manipuler de façon performante un très grand espace d'états. L'avancée par rapport à l'état de l'art a été de proposer de méthodes qui prennent en compte ces fonctions qui expriment des relations entre les composants des modèles. Des études d'exemples sont présentées afin d'illustrer les apports de ces méthodes. Dans la deuxième partie de cette thèse, nous nous sommes intéressés à la résolution d'un modèle SAN à temps discret dont la matrice de transition est représentée par une formule tensorielle (appelée descripteur discret). A cet effet, nous présentons l'Algèbre Tensorielle compleXe (ATX) adaptée à la composition parallèle des SAN à temps discret pour la représentation du descripteur et nous démontrons des propriétés qui servent de base aux méthodes itératives pour la résolution de la chaîne de Markov associée au modèle SAN. Un des avantages de représenter un modèle SAN par un descripteur est la façon compacte par laquelle on peut représenter les transitions du modèle: on remplace une description dans un espace produit par un unique produit tensoriel portant sur des facteurs qui décrivent ce qui se passe sur une seule dimension (une composante du modèle SAN). Afin de profiter de cette représentation, nous présentons une méthode de multiplication d'un vecteur de probabilité par un descripteur discret adaptée à cette algèbre. Cette méthode vise à exploiter des propriétés du produit tensoriel complexe de façon à ce que la multiplication par un opérateur sur l'espace produit soit remplacée par une suite d'opérations qui manipulent des données de la taille d'une composante (et pour toutes les composantes).

Dans un circuit asynchrone, la synchronisation entre les blocs est locale: on s'affranchit ainsi des contraintes liées à l'horloge. Ces circuits sont plus robustes, modulaires, moins bruités, et ont une consommation dynamique plus faible que les circuits synchrones. Cependant, le manque d'outils de conception de tels circuits freine leur développement. Cette thèse a permi de développer une technique de synthèse automatique de circuits asynchrones quasi insensibles aux délais (QDI), qui sont particulièrement robustes. La méthode de synthèse permet de synthétiser un circuit totalement décomposé en portes logiques élémentaires, ce qui permet d'effectuer une projection technologique. De plus, une étude formelle réalisée durant la thèse démontre que les circuits synthétisés respectent la contrainte de quasi insensibilité aux délais. Cette technique de synthèse a été développé au sein du projet TAST. Elle a été validée sur un ensemble de circuits de tests.