在分布式并发系统构造过程中,基于进程代数的并发系统模型检测是一种行之有效的减少设计错误、提高系统可靠性的重要途径。但并发系统本身随着规模增大其状态呈指数剧增,产生的状态爆炸问题成了模型检测在实际应用中的绊脚石。实践表明,对并发系统进行性质验证出现的状态爆炸问题需要进行深入研究。 本文分析了模型检测中状态爆炸的成因,然后针对状态爆炸问题提出相应的模型检测方法。主要包括三个方面的工作: 1.分析了状态爆炸的成因,提出了一种有效的安全性和活性验证方法,在此方法上提出基于假设的状态约减算法(简称ABSR),将性质验证放在容易产生状态爆炸的环节上,限制子系统的交互环境从而避免冗余状态剧增。 2.分析了并发系统迁移之间的依赖关系,提出基于进程代数的偏序简化技术。不仅能更大程度上限制并发系统模型的状态空间,而且保留了冗余状态信息,在需要时可根据其将冗余状态恢复出来。最后在偏序简化技术基础上提出相应的安全性验证算法。 3.设计了支持上述算法的原型系统VerTool,分析了并发模型的五种进程并发合成类型,对每一种类型用VerTool进行测试并比较了算法验证前后的结果的化简效率。在保证并发系统性质验证结果正确的同时,提高了并发系统模型检测的效率。 实验数据表明,采用ABSR方法的VerTool能够大幅度约减模型组合过程产生的冗余状态,使得模型的状态增长方式从指数转为线性;采用基于进程代数的偏序简化可以精简模型的所有冗余状态,效果更强于ABSR;由于保留了被精简掉的冗余状态信息,所以根据需要还可以恢复出这些状态并参与高一层的模型组合。总之,偏序简化技术有效地解决了模型检测在实际应用中遇到的状态爆炸问题。