Title :
Advanced modelling and verification techniques applied to a cluster file system
Author :
Pecheur, Charles
Author_Institution :
Res. Inst. for Adv. Comput. Sci., NASA Ames Res. Center, Moffett Field, CA, USA
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
Keywords :
distributed databases; formal specification; network operating systems; program verification; shared memory systems; temporal logic; CADP toolset; XTL; cluster file system; data-aware temporal logic checker; distributed file system kernel; formal modelling; model generation; verification techniques; Cryptographic protocols; Design methodology; Explosions; File systems; Memory architecture; NASA; Read only memory; Specification languages; State-space methods; Writing;
Conference_Titel :
Automated Software Engineering, 1999. 14th IEEE International Conference on.
Conference_Location :
Cocoa Beach, FL
Print_ISBN :
0-7695-0415-9
DOI :
10.1109/ASE.1999.802152
