针对科学实验载荷使用的Linux操作系统,对其测试方法等做了研究总结。模型检测作为一种全自动运行的形式化验证手段,在其适用领域对发现系统逻辑错误意义重大。针对操作系统测试需要,对Linux管道通信进行了源代码研究,使用有限状态自动机进行建模并转化为Promela语言,并运用SPIN模型检测工具对其进行了形式化验证;对之前研究中模型不完整、不够细化、主体间关联性等问题进行了改进和完善,并就实验中发现的问题进行分析,并提出了改进方案。