网络环境下的分布式系统是典型的并发系统。安全性和活性是并发系统最为关注和需要保证的两个主要性质。然而在并发系统建模和形式化验证时，面临着描述繁琐、复杂和难以理解的问题，特别是当并发系统的规模（并发进程数目）较大时其性质验证时的效率问题更是严重阻碍了并发系统模型检测与验证技术的应用。将组合可达性分析和标号迁移系统的模块化思想与模型验证技术相结合，提出了一套有效的性质验证方法。论证、分析了三个并发系统安全性和活性验证定理，据此导出了并发系统的安全性与活性验证的有效算法。并通过一个简单实例，对算法有效性进行了初步验证。