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

fYear

1999

fDate

36434

Firstpage

119

Lastpage

126

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 1999. 14th IEEE International Conference on.

Conference_Location

Cocoa Beach, FL

Print_ISBN

0-7695-0415-9

Type

conf

DOI

10.1109/ASE.1999.802152

Filename

802152