Ces travaux portent sur la validation de modèles de systèmes sur puce (SoC) au niveau transactionnel (TLM). Ces modèles servent notamment au développement du logiciel embarqué. Le matériel est intrinsèquement parallèle mais le simulateur utilise un seul processeur. Les principales entités parallèles du matériel (processeurs, DMA, arbitres de bus, ...) sont représentées en TLM par des processus asynchrones, qui doivent être ordonnancés lors des simulations. Cet ordonnancement est indéterministe afin de mieux représenter le parallélisme physique.<br /><br />Cela pose un problème pour la validation par simulations : il faut couvrir l'espace des ordonnancements en plus de celui des données. En effet, un ordonnanceur déterministe peut cacher des erreurs, car il ne montre qu'un comportement parmi d'autres. Des ordonnancements aléatoires permettent d'observer plus de comportements mais la couverture est incertaine. Un parcours exhaustif de tous les ordonnancements serait beaucoup trop long pour des tests réels.<br /><br />Nous présentons une solution pour couvrir efficacement l'espace des ordonnancements. Celle-ci est basée sur de la réduction d'ordre partiel dynamique. L'idée est d'observer l'influence de l'ordonnancement sur les communications entre processus, pour générer dynamiquement de nouveaux ordonnancements, menant très probablement à des états finaux différents. En itérant sur chaque nouvel ordonnancement, nous obtenons un jeu complet d'ordonnancements, qui garantit la détection, pour un jeu fixé de données, de toutes les erreurs locales et de tous les inter-blocages.<br /><br />Toujours avec l'objectif d'une meilleure représentativité du matériel, les développeurs ont ajouté du temps imprécis à leurs modèles TLM, sous forme de délais bornés. Pour la validation par simulations, cela oblige à couvrir aussi l'espace des temporisations. Nous présentons une extension à la réduction d'ordre partiel dynamique pour résoudre ce problème. Le nouvel algorithme et son prototype retournent un ensemble de jeux de durées, qui garantit de nouveau la détection complète des erreurs locales et inter-blocages pour des données fixées.<br /><br />Enfin, nous étudions comment paralléliser le simulateur SystemC afin de profiter des machines multiprocesseurs, tout en respectant la spécification de SystemC et les particularités des modèles TLM.

La vérification des systèmes d'états finis, qu'ils soient distribués ou concurrents, est confrontée en pratique au problème d'explosion d'états (taille prohibitive de l'espace d'états sous-jacent) qui survient pour des systèmes de taille réaliste, contenant de nombreux processus en parallèle et des structures de données complexes. Différentes techniques ont été proposées pour combattre l'explosion d'états, telles que la vérification à la volée, la réduction d'ordre partiel, ou encore la vérification distribuée. Cependant, l'expérience pratique a montré qu'aucune de ces techniques, à elle seule, n'est toujours suffisante pour maîtriser des systèmes à grande échelle. Cette thèse propose une combinaison de ces approches dans le but de faire passer à l'échelle leurs capacités de vérification. Notre approche est basée sur les Systèmes d'Equations Booléennes (SEBs), qui fournissent une représentation intermédiaire élégante des problèmes de vérification définis sur des Systèmes de Transitions Etiquetées, comme la comparaison par équivalence, la réduction par tau-confluence, l'évaluation de formules de mu-calcul modal sans alternance, ou encore la génération de cas de tests de conformité. Nous proposons DSolve et MB-DSolve, deux nouveaux algorithmes pour la résolution distribuée à la volée de SEBs (contenant un, resp. plusieurs blocs d'équations), et nous les employons comme moteurs de calcul pour quatre outils de vérification à la volée développés au sein de la boîte à outils CADP en utilisant l'environnement OPEN/CAESAR : le comparateur par équivalence BISIMULATOR, le réducteur TAU_CONFLUENCE, l'évaluateur de propriétés temporelles EVALUATOR, et le générateur de cas de tests de conformité EXTRACTOR. Les mesures expérimentales effectuées sur des grappes de machines montrent des accélérations quasi-linéaires et un bon passage à l'échelle des versions distribuées de ces outils par rapport à leurs équivalents séquentiels.