Paper Info
Title
Advanced Modelling and Verification Techniques Applied to a Cluster File System
Abstract
This paper describes the application of advanced formal modelling techniques and tools from the CADP toolset to the verification of CFS, a distributed file system kernel. After a short overview of the specification of CFS, we describe the techniques used for model generation and verification, 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 verify properties of the system. In particular, an XTL extension providing richer diagnostics is presented. (This research was performed at and for INRIA Rhone-Alpes, France, and is not connected to any RIACS and NASA activity.)
Year
DOI
Venue
1999
10.1109/ASE.1999.802152
ASE '99 Proceedings of the 14th IEEE international conference on Automated software engineering
Keywords
Field
DocType
model generation,inria rhone-alpes,xtl extension,file system kernel,cadp toolset,verification techniques applied,nasa activity,cluster file system,richer diagnostics,original aspect,advanced formal modelling technique,advanced modelling,data-aware temporal logic checker,formal specification,distributed databases,cryptographic protocols,read only memory,design methodology,writing,temporal logic,distributed file system
Kernel (linear algebra),Distributed File System,File system,Model checking,Programming language,Computer science,Formal specification,Formal methods,Distributed database,Temporal logic
Conference
ISBN
Citations 
PageRank 
0-7695-0415-9
6
0.58
References 
Authors
12
1
Name
Order
Citations
PageRank
Charles Pecheur128428.50