由于分布式系统的固有复杂性,结合分布式系统的领域背景来证明和验证分布式系统的功能正确性一直是计算机科学领域的重要问题。机群系统和网格系统均是高度复杂的分布式系统,其中机群文件系统共享语义和网格使用模式的研究分别是涉及各自领域的功能正确性、性能和易用性的关键问题。本文首先从文件系统共享文件语义和计算机使用模式这两个方面系统地综述了机群文件系统语义和网格使用模式领域的主要研究成果。作为本文的研究重点之一,在机群文件系统共享语义研究方面,从文件缓存协议构造、语义正确性证明和共享语义测试等方面对机群文件系统共享语义的关键问题进行了深入探讨。在网格的用户使用模式研究方面,本文对用户和服务网格系统进行理论建模,提出并证明了用户3A使用服务网格必须满足的一些性质和条件。本文创造性的工作主要有三个方面:(1)提出了一种基于POSIX文件锁的缓存一致性协议LBCCP,该协议能够在文件粒度支持动态调整文件共享语义。本文给出了LBCCP协议的I/O自动机模型并证明了LBCCP协议的正确性,在证明过程中找到并改正了DCFS文件系统协议中的几处错误。(2)提出了文件系统共享语义测试概念并实现了一个文件语义测试系统FSbench。FSbench目前能够测试机群文件系统最常用的两种共享语义,分别是UNIX语义和NFS语义。FSbench可用于判断应用程序在不同文件系统无缝移植的可行性和验证新文件系统的语义正确性,我们利用FSbench进行语义测试时发现了DCFS和PVFS在共享语义支持方面的一些问题,改进后的DCFS版本已经能够通过目录的UNIX语义测试。(3)给出了用户3A (Anytime, Anyplace and on Anydevice)使用模式的定义,利用抽象状态机(ASM)理论对用户和服务网格系统进行形式化建模,并证明了服务网格3A使用模式定理。该定理给出了服务网格系统提供3A使用模式的一些充分条件和性质,这些性质可以用于指导实际网格系统的设计和实现。