Les methodes de test de microprocesseurs sont passées en revue et les caractéristiques et l'environnement de test propres à l'usager sont définis. Une methode de test s'appuyant sur une description comportementale des microprocesseurs est proposée; elle se décompose en un test de conformité, Le test de balayage et un test des signaux complémentaires. Un équipement de test expérimental à permis de prouver l'efficacité de l'approche sur des lots de microprocesseurs (MC6800)

Les systèmes logiciels sont devenus omniprésents se substituant à l'homme pour des tâches délicates, souvent critiques, mettant en jeu des coûts importants voire des vies humaines. Les conséquences des défaillances imposent la recherche de méthodes rigoureuses pour la validation. L'approche par automates du model-checking est la plus classique des approches de vérification automatique. Elle prend en entrée un modèle du système et une propriété, et permet de savoir si cette dernière est vérifiée. Pour cela un model-checker traduit la négation de la propriété en un automate et vérifie si le produit du système et de cet automate est vide. Hélas, bien qu'automatique, cette approche souffre d'une explosion combinatoire du nombre d'états du produit.Afin de combattre ce problème, en particulier lors de la vérification des propriétés insensibles au bégaiement, nous proposons la première évaluation d'automates testeur (TA) sur des modèles réalistes, une amélioration de l'algorithme de vérification pour ces automates et une méthode permettant de transformer un TA en un automate (STA) permettant une vérification en une seule passe.Nous proposons aussi une nouvelle classe d'automates: les TGTA. Ces automates permettent une vérification en une seule passe sans ajouter d'états artificiels. Cette classe combine les avantages des TA et des TGBA (automates de Büchi). Les TGTA permettent d'améliorer les approches explicite et symbolique de model-checking. Notamment, en combinant les TGTA avec la saturation, les performances de l'approche symbolique sont améliorées d'un ordre de grandeur par rapport aux TGBA. / Software systems have become ubiquitous in our everyday life. They replace humans for critical tasks that involve high costs and even human lives. The serious consequences caused by the failure of such systems make crucial the use of rigorous methods for system validation. One of the widely-used formal verification methods is the automata-theoretic approach to model checking. It takes as input a model of the system and a property, and answers if the model satisfies or not the property. To achieve this goal, it translates the negation of the property in an automaton and checks whether the product of the model and this automaton is empty. Although it is automatic, this approach suffers from the combinatorial explosion of the resulting product. To tackle this problem, especially when checking stutter-invariant LTL properties, we firstly improve the two-pass verification algorithm of Testing automata (TA), then we propose a transformation of TA into a normal form (STA) that only requires a single-pass verification algorithm.
 We also propose a new type of automata: the TGTA. These automata also enable a check in a single-pass and without adding artificial states : it combines the benefits of TA and generalized Büchi automata (TGBA). TGTA improve the explicit and symbolic model checking approaches. In particular, by combining TGTA with the saturation technique, the performances of the symbolic approach has been improved by an order of magnitude compared to TGBA. Used in hybrid approaches TGTA prove complementary to TGBA.
 All the contributions of this work have been implemented in SPOT and LTS-ITS, respectively, an explicit and a symbolic open source model-checking libraries.

Les travaux présentés dans ce mémoire entrent dans le cadre de la réduction des coûts de production des circuits RF. En effet, la démocratisation de ces appareils pousse les industriels à chercher de nouvelles solutions afin de produire, à bas prix, ces circuits RF. Le test représentant une large partie du coût de ces produits, l'objectif de cette thèse a donc été de proposer une stratégie originale permettant d'effectuer l'analyse de signaux modulés à l'aide d'un équipement de test numérique faible coût. Tout d'abord, le manuscrit dresse un tableau général du test industriel et présente un éventail des solutions proposées dans la littérature pour réduire le coût du test des circuits RF, ainsi que des exemples d'utilisation du concept de " level-crossing ", méthode choisie pour effectuer la capture puis la reconstruction des signaux analogiques et RF. Les principes de base utilisés pour la reconstruction de signaux analogiques à partir d'informations temporelles sont ensuite abordés. L'élément clé des algorithmes de reconstruction est la détermination des instants de passage du signal par un seuil de tension prédéterminé. De cette information, il est ensuite possible de déterminer la phase, la fréquence et l'amplitude du signal observé. La suite est consacrée à l'analyse de signaux modulés. Dans un premier temps sur des modulations élémentaires, puis sur des schémas de modulations plus complexes, basés sur des cas d'étude concrets. Le travail se termine en abordant la prise en compte des non-idéalités de la chaîne d'acquisition. Il s'agit en particulier d'étudier l'impact de ces non-idéalités pour élaborer des algorithmes visant à compenser les erreurs résultantes.