Advanced Modelling and Verification Techniques Applied to a Cluster File System

Charles Pecheur

Proceedings of the 14th IEEE International Conference on Automated Software Engineering ASE-99 (Cocoa Beach, Florida, USA), October 1999.


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.

8 pages


There exists an extended version of this work, available from here.