Database of Case Studies Achieved Using CADP

Cluster File System (CFS)

Organisation: INRIA Rhone-Alpes

Method: LOTOS

Tools used: APERO (data type facilities)
CADP (Construction and Analysis of Distributed Processes)
EUCALYPTUS (graphical user interface)

Domain: Distributed File System.

Period: Jul-Dec 1997.

Size: - 1000 lines of LOTOS (using APERO concise data type definitions)
- 6 man-months.

Description: ARIAS is a shared memory support system implemented in the AIX operating system. The Cluster File System (CFS) is a distributed file system built on top of ARIAS. This case study focuses on the coherency protocol used in CFS. The protocol, together with an abstraction of the underlying ARIAS service, have been specified in LOTOS, with the help of APERO extensions for defining data types. A model has been generated compositionally, by assembling together separately generated models of different sub-components. The XTL extended temporal logic checker has then been used to assert the coherency properties of the protocol on the obtained model. Besides, XTL has been enriched in order to provide diagnostic traces to illustrate its results.

Conclusions: Though model checking is based on autonomous algorithms, a combination of large computing resources, sophisticated tools and skilled formal method experts is still required to master state space explosion. In this respect, this study has benefited from the combined use of two advanced facilities:
  • compositional model generation, in order to produce a model that would have been impossible to generate in a single step,
  • extended temporal logics with support for data types, so that properties about the attributes of LOTOS events can be expressed conveniently, concisely and in their full generality.
The extensions of XTL's functionalities was relatively easy because XTL is an open, programmable tool. The provided extensions provide diagnostic traces at the cost of increased algorithmic complexity.

Publications: [Pecheur-98] Charles Pecheur, Advanced Modelling and Verification Techniques Applied to a Cluster File System. INRIA Research Report 3416, May 1998, 55 pages.
Available on-line from: http://cadp.inria.fr/publications/Pecheur-98.html

[Pecheur-99] Charles Pecheur, Advanced Modelling and Verification Techniques Applied to a Cluster File System. Proceedings of the 14th IEEE International Conference on Automated Software Engineering ASE-99 (Cocoa Beach, Florida, USA), October 1999, 8 pages.
Available on-line at: http://cadp.inria.fr/publications/Pecheur-99.html
Contact:
Charles Pecheur
INRIA Rhone-Alpes
655, avenue de l'Europe
38330 Montbonnot Saint Martin
France
tel : +33-476.61.52.98
fax : +33-476.61.52.52
E-mail : Charles.Pecheur@inria.fr
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page