Vérification formelle des communications dans un réseau sur puce : HERMES à l'aide d'ACL2

Amr Helmy (1)

1 TIMA - Techniques de l'Informatique et de la Microélectronique pour l'Architecture des systèmes intégrés

Pour la conception des systèmes multi-composants complexes (SoCs), une technique largement répandue aujourd'hui est la réutilisation de modules préfabriqués (IPs) interconnectés grâce à un réseau sur puce (NoC). Ce papier s'intéresse à la vérification formelle de réseaux sur puces à l'aide d'un démonstrateur de théorèmes automatique (l'outil ACL2). Dans une précédente thèse, un modèle formel générique pour les NoCs a été proposé et mis en oeuvre dans ACL2, ce papier propose quelques extensions pour ce modèle et décrit la preuve d'un réseau spécifique, HERMES.

Domaines: Réseaux et télécommunications [cs.NI]

Amr Helmy. Vérification formelle des communications dans un réseau sur puce : HERMES à l'aide d'ACL2. Huitièmes Journées Doctorales en Informatique et Réseaux (JDIR'07), Jan 2007, Marne-la-Vallée, France. pp.161-168. ⟨hal-01116655⟩