随着并发软件系统在国民经济、国防等关键领域的广泛应用，如何验证其正确性和可靠性以保证软件质量成为日益紧迫的问题。对并发系统而言，其内在的不确定性使问题的难度更大。通过对并发系统的形式化分析，可以查找出系统设计中的漏洞或缺陷，能够帮助设计者修改和优化系统，使其更规范、有效、合理。可以说形式化方法在软件系统设计的全过程中发挥相当重要的作用。模型检测技术是近二十年来最成功的形式化自动验证技术之一。其因自动化程度高，效率高等优点而被广泛应用于并发系统的分析与验证中。然而模型检测技术的最大障碍是状态爆炸问题——并发系统的状态数量随并发分量的增加呈指数增长。因此本文对并发系统进行模型检测技术以及状态爆炸问题进行了深入研究。主要包括以下四个方面的工作：首先，分析了目前用于形式化描述的语言。以通信系统CCS为代表的进程代数方法，因其概念简洁，可用的数学工具丰富，在并发系统的规范、分析、设计和验证等方面获得了广泛应用。因此，本文决定采用进程代数的形式化描述方法来研究并发系统模型。其次，分析了状态爆炸的成因，将偏序简化技术应用于进程代数模型上。提出了基于进程代数的偏序简化算法，能更大程度上限制并发系统模型的状态空间，有效得提高了性质验证的效率。再次，在偏序简化技术基础上提出了相应的安全性以及死锁性验证算法。并证明了该算法的有效性。最后，设计了支持上述算法的模型检测原型系统MCTool，分析了并发模型的五种进程并发合成简化前后的情况，并使用典型实例，对工具进行了实验验证。实验结果表明在保证并发系统性质验证结果正确的同时，提高了并发系统模型检测的效率。