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

Résumé : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-01116655
Contributor : Admin Ligm <>
Submitted on : Friday, February 13, 2015 - 6:15:44 PM
Last modification on : Wednesday, May 16, 2018 - 6:30:04 PM
Long-term archiving on : Thursday, May 14, 2015 - 11:10:29 AM

File

ACTES_JDIR_2007-20.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-01116655, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

125

Files downloads

87