随着人们对软硬件系统功能需求的日益增加,导致系统的规模越来越复杂,其安全性和可靠性也越来越难以得到保证。在一些关键领域,例如航空航天、银行、证券等,软件可靠性问题显得尤为重要,已经日益成为当今研究的重要课题。在过去的三十几年间,针对并发系统运行的不确定性,各国研究人员为解决可靠性问题做出了许多工作,其中,模型检测验证技术就是该领域中的热点之一。模型检测是一种形式化自动验证技术,它可以为许多软件设计中的相关问题提出解决办法。一般给定一个系统的形式化数学模型以及形式化的规约属性,就可以使用模型检测技术验证该系统是否满足属性。自动检测器的检测结果要不证明该系统满足该属性,要不提供一个反例路径。然而,对于许多类型的系统来说,随着建模系统规模和进程数目的扩大,运行过程中可能产生的状态数将呈指数级增长,这就引起了状态爆炸问题。偏序规约技术就是为了缓解异步并发系统的状态爆炸问题而产生的,该技术主要是构建一个更小的状态空间子集,而搜索时仅探测该状态空间子集,并不是探测所有的并发交错运行。本文中,我们对模型检测技术和偏序规约技术进行深入的研究,主要工作如下:1、详述了并发系统的形式化描述方法及模型检测的一些基本原则,并研究如何使用TLA+语言对现实问题进行规约。2、研究了偏序规约的相关理论,同时对几种约简状态空间的偏序规约算法进行深入研究,包括充足集(ample)、持久集(persistent)、条件顽固集(conditional stubborn)。3、基于条件顽固集和持久集的计算算法,通过集合理论证明了在相同条件下,有条件顽固集算法比持久集算法更加有效。4、结合使用顽固集和对称性约简技术,在Petri网的建模工具基础上,分析了读写互斥算法的约简过程,通过工具LoLA进行实验对比验证。5、研究了偏序规约的实验效果评估,并提出了基于Promela语言的领导选举算法的建模方法,同时利用SPIN工具进行偏序规约。