Specification and Verification of the PowerScale Bus Arbitration Protocol:An Industrial Experiment with LOTOS

Abstract : This paper presents the results of an industrial case-study concerning the use of formal methods for the validation of hardware design. The case-study focuses on PowerScale, a multiprocessor architecture based on PowerPC micro-processors and used in Bull's Escala series of servers and workstations. The specification language LOTOS (ISO International Standard 8807) was used to describe formally the main components of this architecture (processors, memory controller and bus arbiter). Four correctness properties were identified, which express the essential requirements for a proper functioning of the arbitration algorithm, and formalized in terms of bisimulation relations (modulo abstractions) between finite labelled transition systems. Using the compositional and on-the-fly model-checking techniques implemented in the CADP (CAESAR/ALDEBARAN) toolbox, the correctness of the arbitration algorithm was established automatically in a few minutes.
Type de document :
Rapport
[Research Report] RR-2958, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073740
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:39:24
Dernière modification le : mercredi 11 avril 2018 - 01:54:28
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:56:42

Fichiers

Identifiants

  • HAL Id : inria-00073740, version 1

Collections

Citation

Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, Ferruccio Zulian. Specification and Verification of the PowerScale Bus Arbitration Protocol:An Industrial Experiment with LOTOS. [Research Report] RR-2958, INRIA. 1996. 〈inria-00073740〉

Partager

Métriques

Consultations de la notice

260

Téléchargements de fichiers

663