|
| 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
Proceedings of the 14th IEEE International Conference on Automated Software
Engineering ASE-99 (Cocoa Beach, Florida, USA), October 1999.
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.
| 8 pages |  |
 PostScript |
There exists an extended version of this work, available from here.