System Design of a CC-NUMA Multiprocessor Architecture Using Formal Specification, Model-Checking, Co-Simulation, and Test Generation

Hubert Garavel 1 César Viho 2 Massimo Zendri 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 PAMPA - Models and Tools for Programming Distributed Parallel Architectures
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : The application of formal methods to system-level design of hardware components is still an open issue for which concrete case-studies are needed. We present here an industrial experiment concerning the application of the process algebraic language Lotos (ISO standard 8807) to the design of Polykid, a CC-NUMA (Cache Coherent -- Non Uniform Memory Access) multiprocessor architecture developed by Bull. The formal descriptions developed for Polykid have served as a basis not only for model-checking verification using CADP (Caesar/Aldebaran Development Package), but also for hardware-software co-simulation using the Exec/Caesar tool, and for automatic generation of executable tests using the TGV tool.
Type de document :
Rapport
[Research Report] RR-4041, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072597
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:21:48
Dernière modification le : samedi 15 décembre 2018 - 01:49:37
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:14:53

Fichiers

Identifiants

  • HAL Id : inria-00072597, version 1

Citation

Hubert Garavel, César Viho, Massimo Zendri. System Design of a CC-NUMA Multiprocessor Architecture Using Formal Specification, Model-Checking, Co-Simulation, and Test Generation. [Research Report] RR-4041, INRIA. 2000. 〈inria-00072597〉

Partager

Métriques

Consultations de la notice

632

Téléchargements de fichiers

526