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

Hubert Garavel, César Viho, and Massimo Zendri

Springer International Journal on Software Tools for Technology Transfer (STTT), volume 3, number 3, July 2001.

Available as INRIA Research Report RR-4041 (November 2000).

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.

36 pages

PDF

PostScript