-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES)
-- http://cadp.inria.fr

[Last updated: Fri Apr 12 10:43:00 CEST 2024]

TITLE:

  Verification of the coherency protocol of the Cluster File System (CFS).

TOOLS:

  BCG_MIN, CAESAR, EXP/OPEN, SVL, XTL

REFERENCES:
 
  - Jean-Philippe Fassino, Utilisation d'une me'moire virtuelle re'partie
    pour le support d'un syste`me de fichiers re'parti. Master thesis (DEA),
    Universite' Joseph Fourier, Grenoble, June 1996.
 
  - Charles Pecheur, Advanced Modelling and Verification
    Techniques Applied to a Cluster File System, in Proceedings of the
    14th IEEE International Conference on Automated Software Engineering
    ASE-99 (Cocoa Beach, Florida, USA), October 1999.
    Extended version as INRIA Research Report 3416, May 1998.
    See
       http://cadp.inria.fr/publications/Pecheur-98.html
    and
       http://cadp.inria.fr/publications/Pecheur-99.html
    and
       http://cadp.inria.fr/case-studies/98-i-cfs.html
 
FILES:

  cfs.lnt: the source LNT description.

  demo.svl: SVL script that implements the compositional verification.

  macros.xtl: XTL macro-definitions used in demo.svl.

  doc/*.pdf: three documents describing the LOTOS version of the CFS.

  LOTOS/cfs.lotos: the source LOTOS description.

  LOTOS/cfs.t: settings for the PktList hash table. 

INSTRUCTIONS:

Type:
$	svl demo
  or simply:
$	svl

After the verification, you can type
$       svl -clean demo
  or simply:
$       svl -clean
to remove all files produced during the verification.

REMARKS:

* This application uses compositional model generation; the main
  behaviour of the LOTOS description is not used. Trying to generate
  a model for the full description will blow up memory. The main
  behaviour can be explored with OPEN/CAESAR tools such as EXHIBITOR or
  XSIMULATOR (or OCIS), though.
 
* In the default case, the temporal properties are checked on the
  abstract views of the system only (abstract123.bcg, cfs123.bcg, 
  abstract123_12.bcg). XTL can also be applied to the full view 
  (complete123.bcg, see the commented lines at the end of file demo.svl).

  However, this can take a prohibitive time and even exceed the capacities
  of the XTL compiler in some cases. To avoid this, edit the XTL files by
  hand to bypass the checking of all but interesting properties, for which
  the verification is expected to converge rapidly. For convenience two 
  XTL macros 'DO' and 'DONT' have been defined; simply replace 'DO' by 
  'DONT' at the start of undesired properties in order to skip them.

* The LOTOS description has been written using Norman Ramsey's NoWeb
  literate programming system. Both LOTOS/cfs.lotos and doc/cfs.pdf
  have been automatically extracted from a single source document,
  respectively through NoWeb and the APERO data type compiler for
  the former, and through NoWeb and the LaTeX typesetting system for
  the latter.

LIST OF CHANGES:

* The work on this application has been performed by Charles Pecheur from
  July to December 1997 and is described in the above publications by
  Charles Pecheur. This demo example was added to CADP in February 1998. 

* Upgraded by Frederic Lang and Hubert Garavel in March-April 2001. The main 
  improvements are the following (see item #748 in file $CADP/HISTORY for
  details):

  - The Makefile written by Charles Pecheur has been replaced with a
    (much shorter) SVL script.

  - When minimizing LTSs, branching bisimulation (with the BCG_MIN tool)
    is used instead of observational equivalence (with the ALDEBARAN tool).
    As a consequence, the time needed for verification was significantly
    reduced.

* Enhanced by Radu Mateescu in September 2008 and December 2017. The XTL
  files have been corrected and simplified (see items #1310 and #2368 in
  file $CADP/HISTORY for details).

* Upgraded by Wendelin Serwe in June 2009. The "cfs.t" file was added to
  use a hash table to store values of sort PktList (see item #1391 in file
  $CADP/HISTORY for details).

* Simplified by Frederic Lang and Hubert Garavel in March 2015. Many LOTOS
  processes (totalling 155 lines of code) used for compositional verification
  have been removed, thanks to the features of SVL (see file $CADP/demos/
  demo_25/notes.txt and item #2025 in file $CADP/HISTORY for details).

* Further simplified by Hubert Garavel in November 2023. Many LOTOS operations
  and one LOTOS process defined but not used (totalling 205 lines of code)
  have been removed (see file $CADP/demos/demo_25/notes.txt for details).

* In 2022, the LOTOS specification was translated to LNT on the basis of
  a student project done by Oussama Oulkaid et Marck-Edward Kemeh (Univ.
  Grenoble Alpes). Their LNT specification was revised in November 2023
  by Hubert Garavel and modified to ensure strong equivalence with the
  LOTOS specification.