PostScript
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.
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 (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
| 20 pages | |
PostScript |