Specification and Verification of the PowerScale Bus
Arbitration Protocol: An Industrial Experiment with LOTOS
Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, and Ferruccio Zulian
Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV'96 (Kaiserslautern, Germany), pages 435-450, October 1996
Full version available as INRIA Research Report RR-2958.
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 (PowerScale and Escala are registered
trademarks of Bull. PowerPC is a registered trademark of the
International Business Machines Corporation).
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