Coverification des Systemes Integres (French text)

Au cours des décennies passées, la conception des composantes logicielle et matérielle d'un système intégré s'effectuait séparément. Puis, le logiciel (abrégé par L) obtenu était exécuté sur le matériel (abrégé par M) prototype. Si les contraintes de la spécification requises pour le système ne sont pas satisfaites, le processus de conception est réitéré dans l'espoir de retrouver un bon prototype. Afin d'atteindre un niveau maximum de succès, la covérification doit être exécutée en concurrence avec le codesign; en d'autres mots, il est nécessaire qu'elle soit intégrée au codesign dès ses premières phases.; La covérification, a priori, peut être effectuée par trois techniques principales: «bread-boarding», cosimulation et covérification formelle. Nous proposons dans cette thèse d'améliorer cette technique par une méthodologie combinant les concepts de base de la simulation, des inspirations de la vérification formelle et des techniques de la programmation orientée objet.; Notre méthodologie de covérification est basée sur le concept du «multithreading».; La covérification des propriétés susmentionnées est effectuée par un processus de simulation/cosimulation. Étant donné que le système et ses propriétés à covérifier sont répartis en threads, nous amorçons la simulation par une séquence significative de vecteurs de test. Cette séquence devrait être choisie de manière à ce que les propriétés réagissent à l'application de chacun de ses éléments (de la séquence). Les réponses de toutes les propriétés recueillies durant la simulation sont analysées pour conclure des chances de réussite de la covérification. Si une des propriétés a fait preuve d'un comportement incorrect, alors ceci est un signe suffisant de la présence d'une anomalie au sein de l'implémentation (sachant bien sûr que toutes les propriétés sont correctes des points de vue de la syntaxe et de la logique).; Avant de conclure cette thèse, nous avons appliqué notre méthodologie sur un modèle d'un système à plusieurs processeurs et à mémoire partagée afin de contrôler la cohérence des données des différentes caches (chaque processeur en possède une). Nous avons observé et illustré les traces du flux de données du système dans les deux cas: sans et avec protocole de cohérence; les résultats obtenus sont très positifs. Nous avons fait aussi une vérification formelle du même système par la technique de «model checking» offerte par l'outil VIS («Verification Interacting with Synthesis tool») et montré l'aspect de complémentarité entre la covérification et la vérification formelle surtout quand la réalisation de cette dernière s'avère très coûteuse ou impossible. (Abstract shortened by UMI.)...