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