| HAL-Inria | Publications, software ... of Inria's scientists |
Reports
System Design of a CC-NUMA Multiprocessor Architecture Using Formal Specification, Model-Checking, Co-Simulation, and Test Generation
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.
https://hal.inria.fr/inria-00072597
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:21:48 AM
Last modification on : Friday, February 12, 2021 - 3:33:14 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:14:53 PM
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:21:48 AM
Last modification on : Friday, February 12, 2021 - 3:33:14 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:14:53 PM