Advanced Modelling and Verification Techniques Applied to a Cluster File System

Charles Pecheur 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This report describes the application of elaborated formal modelling techniques and tools from the CADP toolset for LOTOS to the validation of CFS, a distributed file system. After a short overview of the LOTOS specification of CFS, we describe the techniques used for model generation and validation, and their application to CFS. Two original aspects are put forth: firstly, the model is generated in a compositional way, by putting together separately generated sub-components; secondly, the extensible, data-aware temporal logic checker XTL is used to express and validate properties of the system. In particular, an XTL extension providing richer diagnostics is presented. The full commented LOTOS specification is provided in appendix.
Type de document :
Rapport
RR-3416, INRIA. 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00073273
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:24:09
Dernière modification le : mercredi 11 avril 2018 - 01:52:17
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:40:44

Fichiers

Identifiants

  • HAL Id : inria-00073273, version 1

Collections

Citation

Charles Pecheur. Advanced Modelling and Verification Techniques Applied to a Cluster File System. RR-3416, INRIA. 1998. 〈inria-00073273〉

Partager

Métriques

Consultations de la notice

270

Téléchargements de fichiers

252