|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
Advanced Modelling and Verification Techniques Applied to a
Cluster File System
Charles Pecheur
INRIA Research report 3416, May 1998
Abstract:
This report describes the application of elaborated formal modelling techniques and tools from the CADP toolset for LOTOS to the validation of CFS, a distributed file system. After a short overview of the LOTOS specification of CFS, we describe the techniques used for model generation and validation, 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 validate properties of the system. In particular, an XTL extension providing richer diagnostics is presented. The full commented LOTOS specification is provided in appendix.
| 55 pages |  |
 PostScript |