Application name:

Bus arbiter of Bull's Powerscale architecture

Organisation:

INRIA Rhone Alpes / DYADE (Bull-INRIA Joint Venture for Advanced Research)

Method:

LOTOS

Tools:

CADP (Caesar/Aldebaran Development Package)

Domain:

Hardware Design.

Period:

• Specification in LOTOS of the whole Powerscale architecture (including time spent in learning both PowerScale and LOTOS): 8 man months
• Specification of the Powerscale bus arbiter: 1.5 man months
• Requirement capture and verification: 1.5 man months

Size:

760 lines of code (26% for the data part and 74% for the control part).

Description:

PowerScale is the multiprocessor, PowerPC-based architecture used by Bull in its Escala series of workstations and servers. In this case-study, LOTOS was used to describe formally the main components of this architecture (processors, memory controller and bus arbiter).

To express the expected functioning properties of the bus arbiter, we identified four correctness requirements. These requirements were expressed using Labelled Transition Systems (LTSs) and the verification process was based on the comparison of LTSs modulo equivalence or preorder relations.

Conclusions:

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.

The results of this experiment are encouraging. It seems that LOTOS is appropriate for the description of hardware protocols, and that the compositional and on-the-fly verification techniques implemented in the CADP tools allow to deal with mid-size industrial cases involving a fair degree of parallelism

Publications:

Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, and Ferruccio Zulian. "Specification and verification of the powerscale bus arbitration protocol: An industrial experiment with lotos". In: Reinhard Gotzhein and Jan Bredereke, editors, 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. IFIP, October 1996. Full version available as INRIA Research Report RR-2958.
Available on-line at:ftp://ftp.inrialpes.fr/pub/vasy/publications/cadp/Chehaibar-Garavel-et-al-96.ps.Z

Contact:

Name:	Hubert Garavel
Organisation:	INRIA Rhone-Alpes
Address:	655 avenue de l'europe 38330 Montbonnot Saint Martin
Country:	France
Phone number:	+33 (4) 476615224
Fax:	+33 (4) 76615252
E-mail:	Hubert.Garavel@inria.fr
Personal website:	http://www.inrialpes.fr/vasy/cadp.html

URL:

http://www.inrialpes.fr/vasy/cadp.html

Remarks:

-

© copyright 2004 | Formal Methods Europe