Proving And Testing The Functional Correctness Of Distributed Systems

Proving and verification the functional correctness of complex distributed systems in many fields are important research problems in computer science. Both Cluster System and Grid System are very complex distributed systems. Cluster file system sharing semantics and grid utilization mode are key issues that address functional correctness, performance, and usability of cluster system and grid systems, respectively. This dissertation concentrates on specifying and verifying the application characteristic of distributed systems. It first surveys the recent development of file system sharing semantics and grid utilization mode. Then, it addresses the problems of cluster file system sharing semantics, the content of research includes the followings: building the file system cache coherence protocol, proving correctness of file sharing semantics, and file sharing semantics testing. This dissertation also introduces an ASM (Abstract State Machine) model of user and service grid system and discusses some character of service grid.The original ideas in this dissertation are explained in detail.1. A POSIX file lock based cache coherence protocol (LBCCP) is presented, which can tune file sharing semantics dynamically. We prove correctness of LBCCP using I/O automata theory after correcting some errors in original protocol.2. The concept of file sharing semantics test is proposed and a file sharing semantics testing system (FSbench) is implemented. FSbench can be used for UNIX or NFS semantics test. We find some bugs of DCFS and PVFS in file sharing semantics test.3. The definitions of 3A (Any time, Any place and Any device) utilization mode are presented and a formal model of user and service grid system (USG) is built using ASM. Based on USG model and these formal definitions, a theorem on 3A utilization mode is proposed and proved.