Sciweavers

Share
KBSE
1999
IEEE

Advanced Modelling and Verification Techniques Applied to a Cluster File System

10 years 8 months ago
Advanced Modelling and Verification Techniques Applied to a Cluster File System
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. Note This research was performed at and for INRIA Rh^one-Alpes, France, and is not connected to any RIACS and NASA activity.
Charles Pecheur
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where KBSE
Authors Charles Pecheur
Comments (0)
books