Bus arbiter of Bull's Powerscale architecture.

Organisation:	INRIA Rhone Alpes / DYADE (Bull-INRIA Joint Venture for Advanced Research)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
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 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 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 from http://cadp.inria.fr/publications/Chehaibar-Garavel-et-al-96.html and from the CADP Web site in PDF or PostScript
Contact:	Hubert Garavel INRIA Rhone-Alpes 655 avenue de l'europe 38330 Montbonnot Saint Martin France tel : +(33) 4 76 61 52 24 fax : +(33) 4 76 61 52 52 E-mail : Hubert.Garavel@inria.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page