“状态空间爆炸”问题一直是验证领域不可避免的难题。在验证的过程中,我们发现有许多带有参数的性质具有可归纳的特性,例如路径的长度,随机数的取值范围,状态空间的个数,通信的步数等。利用归纳特性我们可以把模型检测技术和归纳证明法结合起来使用。本文选择了两个案例对带参数可归纳性质的验证进行了探讨。案例一涉及的是集成电路领域内的逻辑验证,其中提出的终端性质根据路径的长度具有归纳特性。本文在广义符号轨迹赋值(GSTE)已有理论的基础上,提出了终端满足性算法。本文在相关理论基础上证明了终端满足性算法可以利用归纳特性避免一些冗余的计算,降低计算的复杂性。在Round-Robin仲裁器验证的实验中,实验结果表明枚举法的验证时间是终端满足性算法的3.14倍。另一方面,终端满足性算法可以解决GSTE中提出的强满足性算法的一些限制问题。最后本文对终端满足性算法的合理性和完备性给出了证明。案例二涉及的是RFID系统中安全性和隐私性的研究。随着RFID技术的广泛应用,消费者的隐私安全受到越来越多人的重视。设计安全的认证协议是一种有效的保护手段。与此同时,认证协议的验证工作也不可忽视。虽已有很多形式化的验证模型,但是每种方法都有些缺点。本文主要介绍了随机图法和归纳法两种方法。随机图法较直观、可以量化分析。但是验证规模较小,如果随机数取值范围较大,计算复杂性会呈指数级增长。归纳法利用归纳的特性,基于密码学中IND-CPA安全性标准设计了RFID系统中的(r,s,t)-隐私性实验。归纳法可以不受随机数、通信步数取值范围的影响。本文在此基础上设计了(r,s,t,)-安全性实验。最后对OSK协议、VOSK协议进行了验证分析,得出结论:OSK协议不能抵抗拒绝服务攻击,也不能够抵抗重放攻击。即OSK协议不满足(r,s,t)-隐私性标准,也不满足(r,s,t)-安全性标准。VOSK协议不能抵抗拒绝服务攻击,可以抵抗重放攻击。即VOSK协议虽不满足(r,s,t)-隐私性标准,但是满足(r,s,t)-安全性标准。