Database of Case Studies Achieved Using CADP

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


Last modified: Mon Apr 18 14:01:52 2022.


Back to the CADP case studies page