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.

• Type: Conference
• Year: 1999
• Where: KBSE
• Authors: Charles Pecheur
• Keywords: Distributed File System, Formal Modelling Techniques, KBSE 1999, Logic Checker Xtl, Software Engineering