HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072597
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:21:48 AM
Last modification on : Friday, February 4, 2022 - 3:24:01 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:14:53 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

310

Files downloads

417