INRIA Rhone Alpes / DYADE (Bull-INRIA Joint Venture for Advanced
CADP (Construction and Analysis of Distributed Processes)
760 lines of code :
26% for the data part
74% for the control part.
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.
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.
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 our FTP site in PDF or PostScript
655 avenue de l'europe
38330 Montbonnot Saint Martin
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|