• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 164
  • 82
  • 14
  • Tagged with
  • 263
  • 105
  • 104
  • 102
  • 74
  • 61
  • 45
  • 39
  • 38
  • 38
  • 37
  • 37
  • 35
  • 34
  • 33
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
131

Automates cellulaires : dynamique directionnelle et asymptotique typique

Delacourt, Martin 05 December 2011 (has links)
Les automates cellulaires sont à la fois un modèle de calcul parallèle, un système complexe et un système dynamique. Ils fonctionnent de manière synchrone et en temps discret, leur particularité est que les fonctions qu'ils définissent sont issues de l'application simultanée, en tout point de l'espace, d'une règle d'évolution locale. L'ensemble limite est un objet classique des systèmes dynamiques, c'est l'ensemble des états que le système peut atteindre arbitrairement tard. Il a été très étudié dans le cadre des automates cellulaires, et les résultats sont nombreux. Parmi ces résultats, un théorème de Rice démontré par Jarkko Kari dit que toute propriété des ensembles limites est indécidable. Dans ce mémoire, on ne s'intéresse plus à l'ensemble limite traditionnel, mais à une variante pour laquelle on utilise une mesure sur l'espace des entrées, sélectionnant ainsi les comportements susceptibles d'apparaître arbitrairement tard et souvent. Ce nouvel ensemble, que l'on nomme ensemble mu-limite, a été introduit en 2000 par Petr Kurka et Alejandro Maass. La plupart des résultats sur les ensembles limites ne se transposent pas naturellement. On étudie la famille des ensembles mu-limites d'automates cellulaires. On montre que sous certaines contraintes sur la dynamique, l'ensemble mu-limite peut être entièrement décrit. On classe ainsi les automates en fonction de ces contraintes. Dans le cas général, on montre l'existence d'automates cellulaires ayant comme ensembles mu-limites un grand nombre d'ensembles complexes. On finit par montrer un théorème de Rice pour les ensembles mu-limites d'automates cellulaires: tout propriété non triviale de ces ensembles est indécidable. / Cellular automata are simultaneously a model of parallel computation, a complex system and a dynamical system. They are synchronous and time is discrete. The functions defined by their application is the result of the synchronous application of the same local rule everywhere. The limit set is a classical tool of dynamical systems theory, it is the set of states the system can reach arbitrarily late. It has been studied often in the particular case of cellular automata and there are numerous results. Amongst them, a Rice's theorem proved by Jarkko Kari states that any non-trivial property of limit sets of cellular automata is undecidable. In this thesis, we do not consider the classical limit set, as we add a measure on the space of states of the system. Thus, we get a set which contains behaviors that appear arbitrarily far and often. This set is named mu-limit set and was introduced in 2000 by Petr Kurka and Alejandro Maass. Most of the results on limit sets cannot be directly adapted for mu-limit sets. We study the family of all mu-limit sets of cellular automata. We show that under some constraints on the dynamics, the mu-limit set can be entirely described. We then produce a classification of cellular automata according to these constraints. In the general case, we prove the existence of cellular automata whose mu-limit sets are among a large set of complex sets. We finally prove Rice's theorem for mu-limit sets: any non-trivial property is undecidable.
132

Universalité et complexité des automates cellulaires coagulants / Universality and complexity on freezing cellular automata

Maldonado, Diego 26 November 2018 (has links)
Les automates cellulaires forment une famille bien connue de modèles dynamiques discrets, introduits par S.Ulam et J. von Neumann dans les années 40. Ils ont été étudiés avec succès sous différents points de vue: modélisation, dynamique, ou encore complexité algorithmique. Dans ce travail, nous adoptons ce dernier point de vue pour étudier la famille des automates cellulaires coagulants, ceux dont l’état d’une cellule nepeut évoluer qu’en suivant une relation d’ordre prédéfinie sur l’ensemble de ses états. Nous étudions la complexité algorithmique de ces automates cellulaires de deux points de vue : la capacité de certains automates coagulants à simuler tous les autres automates cellulaires coagulants, appelée universalité intrinsèque, et la complexité temporelle de prédiction de l’évolution d’une cellule à partir d’une configuration finie, appelée complexité de prédiction. Nous montrons que malgré les sévères restrictions apportées par l’ordre sur les états,les automates cellulaires coagulants peuvent toujours exhiber des comportements de grande complexité.D’une part, nous démontrons qu’en dimension deux et supérieure il existe un automate cellulaire coagulants intrinsèquement universel pour les automates cellulaires coagulants en codant leurs états par des blocs de cellules ; cet automate cellulaire effectue au plus deux changements d’états par cellule. Ce résultat est minimal en dimension deux et peut être amélioré en passant à au plus un changement en dimensions supérieures.D’autre part, nous étudions la complexité algorithmique du problème de prédiction pour la famille des automates cellulaires totalistiques à deux états et voisinage de von Neumann en dimension deux. Dans cette famille de 32 automates, nous exhibons deux automates de complexité maximale dans le cas d’une mise à jour synchrone des cellules et nous montrons que dans le cas asynchrone cette complexité n’est atteinte qu’à partir de la dimension trois. Pour presque tous les autres automates de cette famille, nous montrons que leur complexité de prédiction est plus faible (sous l’hypothèse P 6≠NP). / Cellular automata are a well know family of discrete dynamic systems, defined by S. Ulam and J. von Neumannin the 40s. The have been successfully studied from the point of view of modeling, dynamics and computational complexity. In this work, we adopt this last point of view to study the family of freezing cellular automata, those where the state of a cell can only evolve following an order relation on the set of states. We study the complexity of these cellular automata from two points of view, the ability of some freezing cellular automata to simulate every other freezing cellular automata, called intrinsic universality, and the time complexity to predict the evolution of a cell starting from a given finite configuration, called prediction complexity. We show that despite the severe restriction of the ordering of states, freezing cellular automata can still exhibit highly complex behaviors.On the one hand, we show that in two or more dimensions there exists an intrinsically universal freezing cellular automaton, able to simulate any other freezing cellular automaton by encoding its states into blocks of cells, where each cell can change at most twice. This result is minimal in dimension two and can be even simplified to one change per cell in higher dimensions.On the other hand, we extensively study the computational complexity of the prediction problem for totalistic freezing cellular automata with two states and von Neumann neighborhood in dimension two. In this family of 32 cellular automata, we find two automata with the maximum complexity for classical synchronous cellular automata, while in the case of asynchronous evolution, the maximum complexity can only be achived in dimension three. For most of the other automata of this family, we show that they have a lower complexity (assuming P 6≠NP).
133

Formal methods for distributed real-time systems / Méthodes formelles pour les systèmes distribués temps-réel

Dellabani, Mahieddine 31 October 2018 (has links)
Nowadays, real-time systems are ubiquitous in several application domains.Such an emergence led to an increasing need of performance (resources,availability, concurrency, etc.) and initiated a shift from theuse of single processor based hardware platforms, to large setsof interconnected and distributed computing nodes. This trend introduced the birthof a new family of systems that are intrinsically distributed, namelyemph{Networked Embedded Systems}.Such an evolution stems from the growing complexity of real-time softwareembedded on such platforms (e.g. electronic control in avionicsand automotive domains), and the need to integrate formerly isolated systems so thatthey can cooperate, as well as share resources improving thus functionalitiesand reducing costs.Undoubtedly, the design, implementation and verification of such systems areacknowledged to be very hard tasks since theyare prone to different kinds of factors, such as communication delays, CPU(s)speed or even hardware imprecisions, which increases considerably the complexity ofcoordinating parallel activities.In this thesis, we propose a rigorous design flow intended forbuilding distributed real-time applications.We investigate timed automata based models, with formally defined semantics, in orderto study the behavior of a given system with some imposed timing constraints when deployedin a distributed environment. Particularly, we study emph{(i)} the impact of the communicationdelays by introducing a minimum latency between actions executions and the effectivedate at which actions executions have been decided,and emph{(ii)} the effect of hardware imperfections, more precisely clocks imprecisions,on systems execution by breaking the perfect clocks hypothesis, often adopted duringthe modeling phase. Nevertheless, timed automata formalism is intended to describe a highlevel abstraction of the behavior of a given application.Therefore, we use an intermediate representation ofthe initial application that, besides having say{equivalent} behavior, explicitly expressesimplementation mechanisms, and thus reduces the gap between the modeling and the concreteimplementation. Additionally, we contribute in building such systems by emph{(iii)}proposing a knowledge based optimization method that aims to eliminate unnecessarycomputation time or exchange of messages during the execution.We compare the behavior of each proposed model to the initial high level model and study therelationships between both. Then, we identify and formally characterize the potential problemsresulting from these additional constraints. Furthermore, we propose execution strategies thatallow to preserve some desired properties and reach a say{similar} execution scenario,faithful to the original specifications. / Aujourd'hui, les systèmes temps réel sont omniprésents dans plusieurs domaines.Une telle expansion donne lieu à un besoin croissant en terme de performance (ressources,disponibilité, parallélisme, etc.) et a initié par la même occasion une transition del'utilisation de plateformes matérielles à processeur unique, à de grands ensemblesde nœuds de calcul inter-connectés et distribués. Cette tendance a donné la naissanceà une nouvelle famille de systèmes connue sous le nom de emph{Networked Embedded Systems},qui sont intrinsèquement distribués.Une telle évolution provient de la complexité croissante des logiciels temps réelembarqués sur de telles plateformes (par exemple les système de contrôle en avioniqueet dans domaines de l'automobile), ainsi que la nécessité d'intégrer des systèmes autrefoisisolés afin d'accomplir les fonctionnalités requises, améliorant ainsi les performanceset réduisant les coûts.Sans surprise, la conception, l'implémentation et la vérification de ces systèmes sontdes tâches très difficiles car ils sont sujets à différents types de facteurs, tels que lesdélais de communication, la fréquence du CPU ou même les imprécisions matérielles,ce qui augmente considérablement la complexité lorsqu'il s'agit de coordonner les activités parallèles.Dans cette thèse, nous proposons une démarche rigoureuse destinée à la construction d'applicationsdistribuées temps réel.Pour ce faire, nous étudions des modèles basés sur les automates temporisés, dont la sémantiqueest formellement définie, afin d'étudier le comportement d'un système donné avec des contraintes de tempsimposées lorsqu'il est déployé dans un environnement distribué. En particulier, nous étudionsemph{(i)} l'impact des délais de communication en introduisant une latence minimale entreles exécutions d'actions et la date à laquelle elles ont été décidées,et emph{(ii)} l'effet des imperfections matérielles, plus précisément les imprécisionsd'horloges, sur l'exécution des systèmes.Le paradigme des automates temporisés reste néanmoins destiné à décrire une abstractiondu comportement d'une application donnée.Par conséquent, nous utilisons une représentation intermédiaire del'application initiale, qui en plus d'avoir un comportement say{équivalent}, exprimeexplicitement les mécanismes mis en œuvre durant l'implémentation, et donc réduit ainsil'écart entre la modélisation et l'implémentation réelle.De plus, nous contribuons à la construction de tels systèmes en emph{(iii)}proposant une optimisation basée sur la emph{connaissance}, qui a pour but d'éliminer lestemps de calcul inutiles et de réduire les échanges de messages pendant l'exécution.  Nous comparons le comportement de chaque modèle proposé au modèle initial et étudionsles relations entre les deux. Ensuite, nous identifions et caractérisons formellement lesproblèmes potentiels résultants de ces contraintes supplémentaires. Aussi, nous proposonsdes stratégies d'exécution qui permettent de préserver certaines propriétés souhaitéeset d'obtenir des scénarios d'exécution say{similaires}, et fidèles aux spécificationsde départs.
134

Discrétisation automatique de machines à signaux en automates cellulaires / Automatic discretization of signal machines into cellular automata

Besson, Tom 10 April 2018 (has links)
Dans le contexte du calcul géométrique abstrait, les machines à signaux ont été développées comme le pendant continu des automates cellulaires capturant les notions de particules, de signaux et de collisions. Une question importante est la génération automatique d’un automate cellulaire reproduisant la dynamique d’une machine à signaux donnée. D’une part, il existe des conversions ad hoc. D’autre part, ce n’est pas toujours possible car certaines machines à signaux présentent des comportements « continus ». Par conséquent, la discrétisation automatique de telles structures est souvent complexe et pas toujours possible. Cette thèse propose trois manières différentes de discrétiser automatiquement les machines à signaux en automates cellulaires, avec ou sans approximation possible. La première s’intéresse à une sous-catégorie de machines à signaux, qui présente des propriétés permettant d’assurer une discrétisation automatique exacte pour toute machine de ce type. La deuxième est utilisable sur toutes les machines mais ne peut assurer ni l’exactitude ni la correction du résultat. La troisième s’appuie sur une nouvelle expression de la dynamique d’une machine à signaux pour proposer une discrétisation. Cette expression porte le nom de modularité et est décrite avant d’être utilisée pour discrétiser. / In the context of abstract geometrical computation, signal machines have been developed as a continuous counter part of cellular automata capturing the notions of particles, signals and collisions. An important issue is the automatic generation of a cellular automaton mimicking the dynamics of a given signal machine. On the one hand, ad hoc conversions exist.On the other hand, it is not always possible since some signal machines exhibit “purely continuous” behaviors. Therefore, automatically discretizing such structures is often complicated and not always possible. This thesis proposes different ways to automatically discretize signal machines into cellular automata, both with and without handling the possiblity of approximation.The first is concerned with a subcategory of signal machines, which has properties ensuring an exact automatic discretization for any machine of this type. The second is usable on all machines but cannot guarantee the exactness and correction of the result. The third is based on a new expression of the dynamics of a signal machine to propose a discretization.This dynamical expression takes the name of modularity and is described before being used to discretize.
135

Mécanismes d'adaptation autonome pour la radio cognitive

Colson, Nicolas 06 May 2009 (has links) (PDF)
La radio cognitive apparaît comme une solution naturelle aux problèmes d'échelle et de complexité résultant de la grande popularité des communications sans fil et de l'évolution des technologies radio. Une radio cognitive est un agent intelligent capable de s'adapter à son contexte opérationnel pour (1) respecter le cadre de régulation contrôlant l'accès au spectre, (2) satisfaire les besoins de l'utilisateur en termes de qualité de service, et (3) assurer une gestion optimisée des ressources disponibles (radios, réseaux et matérielles). Ce nouveau paradigme est directement lié au développement de l'intelligence embarquée, objet de ce travail de thèse.<br /><br />Dans ce mémoire de thèse, nous détaillons la conception d'un moteur cognitif structurant les opérations de raisonnement et d'apprentissage nécessaires à la supervision du processus de reconfiguration dynamique. La solution proposée suit une approche originale basée sur une modélisation qualitative du problème de conception à la volée. <br /><br />Le moteur cognitif raisonne de manière autonome en s'appuyant sur les relations d'ordre définies par deux échelles déduites dynamiquement en fonction du contexte. Il navigue le long de ces deux échelles pour rechercher une configuration adaptée avec un souci d'efficacité et d'optimalité. Il exploite ses capacités de prédiction afin d'estimer l'impact de l'environnement radio sur les performances des configurations disponibles (nombre d'erreurs de transmission tolérables). Il évalue les configurations compatibles avec le service à l'aide d'un système de notation calculant la satisfaction des alternatives vis-à-vis des objectifs d'optimisation (réduire la consommation d'énergie, maximiser le débit de transmission). Si nécessaire, une expérience de conception est déclenchée afin d'explorer l'espace de conception en ligne. Les connaissances mémorisées sont alors mises à l'épreuve dans le but de se rapprocher du comportement optimal. Le plan d'expérience est construit dynamiquement en fonction des retours de l'environnement. Le moteur cognitif profite également de connaissances expertes embarquées pour limiter les risques d'expérimentation. Il accumule de l'expérience progressivement et il apprend à recourir de moins en moins souvent à l'expérimentation pour exploiter ses connaissances devenues fiables.<br /><br />Nous avons testé notre approche sur deux études de cas de conception cognitive d'un lien radio. Les résultats obtenus confirment la pertinence des mécanismes cognitifs proposés. Le moteur cognitif parvient en effet à trouver la solution optimale pour la grande majorité des problèmes traités (95% en moyenne) et il devient de plus en plus efficace dans sa recherche d'une configuration adaptée.<br /><br />Notre méthode combine efficacement la puissance de systèmes d'apprentissage avec des connaissances issues de l'expertise en ingénierie des télécommunications. Le moteur cognitif est conçu avec une grande autonomie décisionnelle grâce à des capacités de raisonnement, d'exploration en ligne et d'apprentissage incrémental. De plus, nous avons proposé des mécanismes avancés pour améliorer son comportement afin d'en faire une solution cognitive effective pour de nombreux problèmes de conception dynamique.
136

Les bassins versants sensibles aux "crues rapides" dans le Bassin Parisien - Analyse de la structure et de la dynamique de systèmes spatiaux complexes

Douvinet, Johnny 02 December 2008 (has links) (PDF)
En raison de leur caractère torrentiel, les « crues rapides » qui apparaissent en périodes printanière et estivale dans les régions du nord de la France constituent aujourd'hui la forme la plus originale et la plus dangereuse des inondations rencontrées dans ces régions. Le poids des activités humaines dans le fonctionnement de ces crises hydrologiques est incontestable. Ces crues turbides prennent naissance sur des territoires agricoles où les espaces cultivés ne cessent de se développer. L'urbanisation croissante et la place du réseau routier dans les axes majeurs d'écoulement aggravent la rapidité des flux et la vulnérabilité des biens et des personnes. Afin d'améliorer la connaissance sur ces événements, un inventaire a été réalisé à partir des dossiers « CatNat ». L'approche comparative menée sur les 189 bassins versants recensés (1983-2005) a permis de faire ressortir l'influence de la morphologie à différentes échelles. La vitesse de concentration de l'écoulement rapide est principalement liée à la combinaison entre le système de pentes, l'organisation des réseaux de talwegs et la forme des bassins versants. Il n'existait cependant aucune méthode permettant de mesurer, de manière synthétique et continue, le rôle de cette composante sur la dynamique hydrologique d'un bassin versant. Les approches quantitatives se sont limitées à des mesures séparées des composantes morphologiques (indices de compacité, rapport de confluence d'Horton, courbe hypsométrique...). En s'appuyant sur la théorie des systèmes complexes, et en particulier sur les automates cellulaires, il a été possible de développer des méthodes permettant de quantifier l'efficacité de la structuration en trois dimensions du « bassin versant ». L'adaptation de ces nouvelles méthodes d'analyse spatiale, encore peu employées en géomorphologie, nécessitera une réflexion sur la validité des outils et la pertinence des<br />résultats en réintégrant progressivement les autres variables de l'hydrosystème. Tous ces résultats aboutissent à la réalisation de différentes cartes de sensibilité dans ces régions du nord de la France.
137

Modélisations par réseaux d'automates cellulaires et simulations parallèles du phénomène de subduction-érosion en tectonique des plaques

Leduc, Thomas 05 July 1999 (has links) (PDF)
Dans cette thèse, nous proposons successivement deux modèles discrets par réseaux d'automates cellulaires, du processus de subduction-érosion en<br />tectonique des plaques, puis présentons les simulations informatiques parallèles correspondantes.<br /><br />Après une présentation de la tectonique des plaques et des marges convergentes de type II (avec érosion), nous présentons les deux tendances de modélisation existantes, étudions leurs avantages et inconvénients respectifs et montrons l'intérêt de développer une démarche radicalement différente. Nous exposons alors nos hypothèses de travail relativement restrictives et leurs limites, en commençant d'abord par présenter la géométrie d'ensemble du "plan de coupe de modélisation" et sa dynamique, puis en énumérant les phénomènes à reproduire, enfin, en introduisant des échelles de temps et la représentation de l'érosion par une altération (un changement de matière) due au vieillissement.<br /><br />En ce qui concerne les modélisations plus précisément, nous nous inspirons très fortement du "Sand Pile Model" uni-dimensionnel pour développer notre propre modèle uni-dimensionnel et introduire la notion de réseau d'automates cellulaires fini généralisé. Dans le cas du modèle bi-dimensionnel, partant du même principe, nous cherchons à implémenter un modèle d'avalanches dans un tas de sable représenté par un réseau d'automates cellulaires bi-dimensionnel. Constatant que la multiplication des informations stockées dans la structure même du réseau offre un meilleur rendu-visuel, nous choisissons alors de généraliser cette méthode et abordons la description de notre propre réseau d'automates cellulaires.<br /><br />Les temps de calcul respectifs de chacune des simulations séquentielles ainsi que le fait que les réseaux d'automates cellulaires constituent un modèle canonique du calcul parallèle à fine granularité, nous incitent à développer des simulations parallèles et à les porter sur des ordinateurs parallèles tels que le CRAY T3E et l'ORIGIN 2000. Après avoir exposé la stratégie de décomposition de domaine que nous avons employée (avec équi-répartition de la charge des sous-domaines sur l'ensemble des processeurs et minimisation de la taille des problèmes aux interfaces), nous montrons l'intérêt d'utiliser une bibliothèque d'échanges de messages appropriée dans le cadre d'une décomposition de domaine régulière sur une architecture parallèle à mémoire distribuée.<br /><br />Les résultats obtenus sont révélateurs (pour la simulation bi-dimensionnelle du moins) de la très bonne parallélisabilité du problème posé. Ils nous permettent de présenter quelques copies d'écran des animations graphiques<br />obtenues et leur validation d'un point de vue géotectonique. Des développements futurs pourraient être orientés vers la mise au point d'une plate-forme logicielle parallèle adaptée, puis vers une étude de qualification de la concentration des déformations au sein de la plaque chevauchante.
138

Méthodes et outils de test pour microprocesseurs et circuits périphériques

Sadier, Sylvain 07 December 1983 (has links) (PDF)
Après avoir situé le problème du test des circuits intégrés, une méthode de test phasée sur une description fonctionnelle du circuit est décrite. le système de test développé en collaboration avec ESD est présente ainsi qu'un outil de description de signaux.
139

Structures arborescentes et apprentissage automatique

Tommasi, Marc 23 November 2006 (has links) (PDF)
Le programme de recherches présenté dans cette synthèse s'inscrit dans la double problématique de l'étude des langages d'arbres et de l'apprentissage automatique à partir de données arborescentes. <br /> À la base de ce travail se trouve la question de l'accès et de la manipulation automatique d'informations au format XML au sein d'un réseau d'applications réparties dans internet. La réalisation de ces applications est toujours du ressort de programmeurs spécialistes d'XML et reste hors de portée de l'utilisateur final. De plus, les développements récents d'internet poursuivent l'objectif d'automatiser les communications entre applications s'échangeant des flux de données XML. Le recours à des techniques d'apprentissage automatique est une réponse possible à cette situation. <br /> Nous considèrons que les informations sont décrites dans un langage XML, et dans la perspective de ce mémoire, embarquées dans des données structurées sous forme arborescente. Les applications sont basées alors sur des opérations élémentaires que sont l'interrogation ou les requêtes dans ces documents arborescents ou encore la transformation de tels documents. <br /> Nous abordons alors la question sous l'angle de la réalisation automatique de programmes d'annotation d'arbres, permettant de dériver des procédures de transformation ou d'exécution de requêtes. Le mémoire décrit les contributions apportées pour la manipulation et l'apprentissage d'ensembles d'arbres d'arité non bornée (comme le sont les arbres XML), et l'annotation par des méthodes de classification supervisée ou d'inférence statistique.
140

Exploration implicite et explicite de l'espace d'´etats atteignables de circuits logiques Esterel

BRES, Yannis 12 December 2002 (has links) (PDF)
Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide de<br />techniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.<br />Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.<br />Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles.<br />Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui<br />confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.<br />Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séequences de tests exhaustives.<br />Nous présentons des résultats d'expérimentations de ces différentes approches sur plusieurs exemples industriels.

Page generated in 0.0498 seconds