Abstract:
In this dissertation, the architecture of the existing file systems such as EXT, NTFS and UFS is
reviewed. A study of space utilization patterns in different file systems has been presented.
Effects of directory depth on file access have been discussed. Moreover, the use of formal
approaches in design and verifications of parallel file systems are presented. Prototype
verification system (PVS) is used as a tool to specify and verify the file system architecture.
We used a top down approach to formalize the hierarchical file systems. The most important
aspects of a file system such as read, write, delete and move are formalized using refinement
techniques where abstract definitions of these operations are specified and then refined towards
a pointer based application. Furthermore, formal specification and verification of the cyclic
data striping algorithm for parallel file systems have been presented with the help of proof
assistant PVS. Our study of applying formal methods to parallel file system design opens many
new directions for the future research. Formalizing the complete parallel file system is a grand
challenge for the scientific community. The hard links and file system security must be
formally designed and verified for building robust, reliable and error free parallel file system
architectures. Several different algorithms for tree structure organization of data files must be
formally verified before use in parallel file systems.
