APERO (data type facilities)
CADP (Construction and Analysis of Distributed Processes)
EUCALYPTUS (graphical user interface)
Distributed File System.
- 1000 lines of LOTOS (using APERO concise data type definitions)
- 6 man-months.
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.
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:
[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
655, avenue de l'Europe
38330 Montbonnot Saint Martin
tel : +33-4126.96.36.199
fax : +33-4188.8.131.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|