Advanced Modelling and Verification Techniques Applied to a Cluster File System

DOI 10.1109/ase.1999.802152 dblp

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.

BibTeX

@inproceedings{Pecheur:ASE99,
  author    = {Charles Pecheur},
  title     = {Advanced Modelling and Verification Techniques Applied to a Cluster File System},
  booktitle = {ASE},
  pages     = {119--126},
  publisher = {{IEEE} Computer Society},
  year      = {1999},
}

Advanced Modelling and Verification Techniques Applied to a Cluster File System

Abstract

Related papers